Step | Hyp | Ref
| Expression |
1 | | epweon 6983 |
. . . . . 6
⊢ E We
On |
2 | | wess 5101 |
. . . . . 6
⊢ (𝐴 ⊆ On → ( E We On
→ E We 𝐴)) |
3 | 1, 2 | mpi 20 |
. . . . 5
⊢ (𝐴 ⊆ On → E We 𝐴) |
4 | | epse 5097 |
. . . . 5
⊢ E Se
𝐴 |
5 | | oismo.1 |
. . . . . 6
⊢ 𝐹 = OrdIso( E , 𝐴) |
6 | 5 | oiiso2 8436 |
. . . . 5
⊢ (( E We
𝐴 ∧ E Se 𝐴) → 𝐹 Isom E , E (dom 𝐹, ran 𝐹)) |
7 | 3, 4, 6 | sylancl 694 |
. . . 4
⊢ (𝐴 ⊆ On → 𝐹 Isom E , E (dom 𝐹, ran 𝐹)) |
8 | 5 | oicl 8434 |
. . . . 5
⊢ Ord dom
𝐹 |
9 | 5 | oif 8435 |
. . . . . . 7
⊢ 𝐹:dom 𝐹⟶𝐴 |
10 | | frn 6053 |
. . . . . . 7
⊢ (𝐹:dom 𝐹⟶𝐴 → ran 𝐹 ⊆ 𝐴) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
⊢ ran 𝐹 ⊆ 𝐴 |
12 | | id 22 |
. . . . . 6
⊢ (𝐴 ⊆ On → 𝐴 ⊆ On) |
13 | 11, 12 | syl5ss 3614 |
. . . . 5
⊢ (𝐴 ⊆ On → ran 𝐹 ⊆ On) |
14 | | smoiso2 7466 |
. . . . 5
⊢ ((Ord dom
𝐹 ∧ ran 𝐹 ⊆ On) → ((𝐹:dom 𝐹–onto→ran 𝐹 ∧ Smo 𝐹) ↔ 𝐹 Isom E , E (dom 𝐹, ran 𝐹))) |
15 | 8, 13, 14 | sylancr 695 |
. . . 4
⊢ (𝐴 ⊆ On → ((𝐹:dom 𝐹–onto→ran 𝐹 ∧ Smo 𝐹) ↔ 𝐹 Isom E , E (dom 𝐹, ran 𝐹))) |
16 | 7, 15 | mpbird 247 |
. . 3
⊢ (𝐴 ⊆ On → (𝐹:dom 𝐹–onto→ran 𝐹 ∧ Smo 𝐹)) |
17 | 16 | simprd 479 |
. 2
⊢ (𝐴 ⊆ On → Smo 𝐹) |
18 | 11 | a1i 11 |
. . 3
⊢ (𝐴 ⊆ On → ran 𝐹 ⊆ 𝐴) |
19 | | simprl 794 |
. . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝑥 ∈ 𝐴) |
20 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → E We 𝐴) |
21 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → E Se 𝐴) |
22 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (𝐹:dom 𝐹⟶𝐴 → 𝐹 Fn dom 𝐹) |
23 | 9, 22 | mp1i 13 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝐹 Fn dom 𝐹) |
24 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → ¬ 𝑥 ∈ ran 𝐹) |
25 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → E We 𝐴) |
26 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → E Se 𝐴) |
27 | | simplrl 800 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ 𝐴) |
28 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑦 ∈ dom 𝐹) |
29 | 5 | oiiniseg 8438 |
. . . . . . . . . . . . . . . . 17
⊢ ((( E We
𝐴 ∧ E Se 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝐹)) → ((𝐹‘𝑦) E 𝑥 ∨ 𝑥 ∈ ran 𝐹)) |
30 | 25, 26, 27, 28, 29 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) E 𝑥 ∨ 𝑥 ∈ ran 𝐹)) |
31 | 30 | ord 392 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → (¬ (𝐹‘𝑦) E 𝑥 → 𝑥 ∈ ran 𝐹)) |
32 | 24, 31 | mt3d 140 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) E 𝑥) |
33 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
34 | 33 | epelc 5031 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑦) E 𝑥 ↔ (𝐹‘𝑦) ∈ 𝑥) |
35 | 32, 34 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ 𝑥) |
36 | 35 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → ∀𝑦 ∈ dom 𝐹(𝐹‘𝑦) ∈ 𝑥) |
37 | | ffnfv 6388 |
. . . . . . . . . . . 12
⊢ (𝐹:dom 𝐹⟶𝑥 ↔ (𝐹 Fn dom 𝐹 ∧ ∀𝑦 ∈ dom 𝐹(𝐹‘𝑦) ∈ 𝑥)) |
38 | 23, 36, 37 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝐹:dom 𝐹⟶𝑥) |
39 | 9, 22 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝐹 Fn dom 𝐹) |
40 | 17 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → Smo 𝐹) |
41 | | smogt 7464 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn dom 𝐹 ∧ Smo 𝐹 ∧ 𝑦 ∈ dom 𝐹) → 𝑦 ⊆ (𝐹‘𝑦)) |
42 | 39, 40, 28, 41 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑦 ⊆ (𝐹‘𝑦)) |
43 | | ordelon 5747 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord dom
𝐹 ∧ 𝑦 ∈ dom 𝐹) → 𝑦 ∈ On) |
44 | 8, 28, 43 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑦 ∈ On) |
45 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝐴 ⊆ On) |
46 | 45, 27 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ On) |
47 | | ontr2 5772 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On) → ((𝑦 ⊆ (𝐹‘𝑦) ∧ (𝐹‘𝑦) ∈ 𝑥) → 𝑦 ∈ 𝑥)) |
48 | 44, 46, 47 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → ((𝑦 ⊆ (𝐹‘𝑦) ∧ (𝐹‘𝑦) ∈ 𝑥) → 𝑦 ∈ 𝑥)) |
49 | 42, 35, 48 | mp2and 715 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑦 ∈ 𝑥) |
50 | 49 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → (𝑦 ∈ dom 𝐹 → 𝑦 ∈ 𝑥)) |
51 | 50 | ssrdv 3609 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → dom 𝐹 ⊆ 𝑥) |
52 | 19, 51 | ssexd 4805 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → dom 𝐹 ∈ V) |
53 | | fex2 7121 |
. . . . . . . . . . 11
⊢ ((𝐹:dom 𝐹⟶𝑥 ∧ dom 𝐹 ∈ V ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ V) |
54 | 38, 52, 19, 53 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝐹 ∈ V) |
55 | 5 | ordtype2 8439 |
. . . . . . . . . 10
⊢ (( E We
𝐴 ∧ E Se 𝐴 ∧ 𝐹 ∈ V) → 𝐹 Isom E , E (dom 𝐹, 𝐴)) |
56 | 20, 21, 54, 55 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝐹 Isom E , E (dom 𝐹, 𝐴)) |
57 | | isof1o 6573 |
. . . . . . . . 9
⊢ (𝐹 Isom E , E (dom 𝐹, 𝐴) → 𝐹:dom 𝐹–1-1-onto→𝐴) |
58 | | f1ofo 6144 |
. . . . . . . . 9
⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹:dom 𝐹–onto→𝐴) |
59 | | forn 6118 |
. . . . . . . . 9
⊢ (𝐹:dom 𝐹–onto→𝐴 → ran 𝐹 = 𝐴) |
60 | 56, 57, 58, 59 | 4syl 19 |
. . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → ran 𝐹 = 𝐴) |
61 | 19, 60 | eleqtrrd 2704 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝑥 ∈ ran 𝐹) |
62 | 61 | expr 643 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 ∈ ran 𝐹 → 𝑥 ∈ ran 𝐹)) |
63 | 62 | pm2.18d 124 |
. . . . 5
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran 𝐹) |
64 | 63 | ex 450 |
. . . 4
⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ ran 𝐹)) |
65 | 64 | ssrdv 3609 |
. . 3
⊢ (𝐴 ⊆ On → 𝐴 ⊆ ran 𝐹) |
66 | 18, 65 | eqssd 3620 |
. 2
⊢ (𝐴 ⊆ On → ran 𝐹 = 𝐴) |
67 | 17, 66 | jca 554 |
1
⊢ (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴)) |