Step | Hyp | Ref
| Expression |
1 | | cofsmo.1 |
. . . . . . . . . . . . 13
⊢ 𝐶 = {𝑦 ∈ 𝐵 ∣ ∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦)} |
2 | | ssrab2 3650 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ 𝐵 ∣ ∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦)} ⊆ 𝐵 |
3 | 1, 2 | eqsstri 3598 |
. . . . . . . . . . . 12
⊢ 𝐶 ⊆ 𝐵 |
4 | | ssexg 4732 |
. . . . . . . . . . . 12
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ On) → 𝐶 ∈ V) |
5 | 3, 4 | mpan 702 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → 𝐶 ∈ V) |
6 | | onss 6882 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) |
7 | 3, 6 | syl5ss 3579 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ On → 𝐶 ⊆ On) |
8 | | epweon 6875 |
. . . . . . . . . . . 12
⊢ E We
On |
9 | | wess 5025 |
. . . . . . . . . . . 12
⊢ (𝐶 ⊆ On → ( E We On
→ E We 𝐶)) |
10 | 7, 8, 9 | mpisyl 21 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → E We 𝐶) |
11 | | cofsmo.3 |
. . . . . . . . . . . 12
⊢ 𝑂 = OrdIso( E , 𝐶) |
12 | 11 | oiiso 8325 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ V ∧ E We 𝐶) → 𝑂 Isom E , E (dom 𝑂, 𝐶)) |
13 | 5, 10, 12 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → 𝑂 Isom E , E (dom 𝑂, 𝐶)) |
14 | 13 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂 Isom E , E (dom 𝑂, 𝐶)) |
15 | | isof1o 6473 |
. . . . . . . . 9
⊢ (𝑂 Isom E , E (dom 𝑂, 𝐶) → 𝑂:dom 𝑂–1-1-onto→𝐶) |
16 | | f1ofo 6057 |
. . . . . . . . 9
⊢ (𝑂:dom 𝑂–1-1-onto→𝐶 → 𝑂:dom 𝑂–onto→𝐶) |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂:dom 𝑂–onto→𝐶) |
18 | | fof 6028 |
. . . . . . . . 9
⊢ (𝑂:dom 𝑂–onto→𝐶 → 𝑂:dom 𝑂⟶𝐶) |
19 | | fss 5969 |
. . . . . . . . 9
⊢ ((𝑂:dom 𝑂⟶𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝑂:dom 𝑂⟶𝐵) |
20 | 18, 3, 19 | sylancl 693 |
. . . . . . . 8
⊢ (𝑂:dom 𝑂–onto→𝐶 → 𝑂:dom 𝑂⟶𝐵) |
21 | 17, 20 | syl 17 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂:dom 𝑂⟶𝐵) |
22 | 11 | oion 8324 |
. . . . . . . . . 10
⊢ (𝐶 ∈ V → dom 𝑂 ∈ On) |
23 | 5, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → dom 𝑂 ∈ On) |
24 | 23 | ad2antlr 759 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → dom 𝑂 ∈ On) |
25 | | simplr 788 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝐵 ∈ On) |
26 | | eloni 5650 |
. . . . . . . . . . 11
⊢ (dom
𝑂 ∈ On → Ord dom
𝑂) |
27 | | smoiso2 7353 |
. . . . . . . . . . 11
⊢ ((Ord dom
𝑂 ∧ 𝐶 ⊆ On) → ((𝑂:dom 𝑂–onto→𝐶 ∧ Smo 𝑂) ↔ 𝑂 Isom E , E (dom 𝑂, 𝐶))) |
28 | 26, 7, 27 | syl2an 493 |
. . . . . . . . . 10
⊢ ((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) → ((𝑂:dom 𝑂–onto→𝐶 ∧ Smo 𝑂) ↔ 𝑂 Isom E , E (dom 𝑂, 𝐶))) |
29 | 28 | biimpar 501 |
. . . . . . . . 9
⊢ (((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑂 Isom E , E (dom 𝑂, 𝐶)) → (𝑂:dom 𝑂–onto→𝐶 ∧ Smo 𝑂)) |
30 | 29 | simprd 478 |
. . . . . . . 8
⊢ (((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑂 Isom E , E (dom 𝑂, 𝐶)) → Smo 𝑂) |
31 | 24, 25, 14, 30 | syl21anc 1317 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Smo 𝑂) |
32 | | eloni 5650 |
. . . . . . . 8
⊢ (𝐵 ∈ On → Ord 𝐵) |
33 | 32 | ad2antlr 759 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Ord 𝐵) |
34 | | smorndom 7352 |
. . . . . . 7
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ Smo 𝑂 ∧ Ord 𝐵) → dom 𝑂 ⊆ 𝐵) |
35 | 21, 31, 33, 34 | syl3anc 1318 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → dom 𝑂 ⊆ 𝐵) |
36 | | onsssuc 5730 |
. . . . . . 7
⊢ ((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) → (dom 𝑂 ⊆ 𝐵 ↔ dom 𝑂 ∈ suc 𝐵)) |
37 | 24, 25, 36 | syl2anc 691 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (dom 𝑂 ⊆ 𝐵 ↔ dom 𝑂 ∈ suc 𝐵)) |
38 | 35, 37 | mpbid 221 |
. . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → dom 𝑂 ∈ suc 𝐵) |
39 | 38 | adantrr 749 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → dom 𝑂 ∈ suc 𝐵) |
40 | | vex 3176 |
. . . . . 6
⊢ 𝑓 ∈ V |
41 | 11 | oiexg 8323 |
. . . . . . . 8
⊢ (𝐶 ∈ V → 𝑂 ∈ V) |
42 | 5, 41 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ On → 𝑂 ∈ V) |
43 | 42 | ad2antlr 759 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → 𝑂 ∈ V) |
44 | | coexg 7010 |
. . . . . 6
⊢ ((𝑓 ∈ V ∧ 𝑂 ∈ V) → (𝑓 ∘ 𝑂) ∈ V) |
45 | 40, 43, 44 | sylancr 694 |
. . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (𝑓 ∘ 𝑂) ∈ V) |
46 | | simprl 790 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → 𝑓:𝐵⟶𝐴) |
47 | 21 | adantrr 749 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → 𝑂:dom 𝑂⟶𝐵) |
48 | | fco 5971 |
. . . . . . 7
⊢ ((𝑓:𝐵⟶𝐴 ∧ 𝑂:dom 𝑂⟶𝐵) → (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴) |
49 | 46, 47, 48 | syl2anc 691 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴) |
50 | | simpr 476 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑓:𝐵⟶𝐴) |
51 | 50, 21, 48 | syl2anc 691 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴) |
52 | | ordsson 6881 |
. . . . . . . . 9
⊢ (Ord
𝐴 → 𝐴 ⊆ On) |
53 | 52 | ad2antrr 758 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝐴 ⊆ On) |
54 | 24, 26 | syl 17 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Ord dom 𝑂) |
55 | 17, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂:dom 𝑂⟶𝐶) |
56 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠) → 𝑠 ∈ dom 𝑂) |
57 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝑂:dom 𝑂⟶𝐶 ∧ 𝑠 ∈ dom 𝑂) → (𝑂‘𝑠) ∈ 𝐶) |
58 | 55, 56, 57 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑂‘𝑠) ∈ 𝐶) |
59 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝑂:dom 𝑂⟶𝐶 → 𝑂 Fn dom 𝑂) |
60 | 17, 18, 59 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂 Fn dom 𝑂) |
61 | 60, 31 | jca 553 |
. . . . . . . . . . . 12
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (𝑂 Fn dom 𝑂 ∧ Smo 𝑂)) |
62 | | smoel2 7347 |
. . . . . . . . . . . 12
⊢ (((𝑂 Fn dom 𝑂 ∧ Smo 𝑂) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑂‘𝑡) ∈ (𝑂‘𝑠)) |
63 | 61, 62 | sylan 487 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑂‘𝑡) ∈ (𝑂‘𝑠)) |
64 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑂‘𝑠) → (𝑓‘𝑧) = (𝑓‘(𝑂‘𝑠))) |
65 | 64 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑂‘𝑠) → ((𝑓‘𝑥) ∈ (𝑓‘𝑧) ↔ (𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)))) |
66 | 65 | raleqbi1dv 3123 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑂‘𝑠) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧) ↔ ∀𝑥 ∈ (𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)))) |
67 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑥 → (𝑓‘𝑤) = (𝑓‘𝑥)) |
68 | 67 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → ((𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ (𝑓‘𝑥) ∈ (𝑓‘𝑦))) |
69 | 68 | cbvralv 3147 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑤 ∈
𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) ∈ (𝑓‘𝑦)) |
70 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → (𝑓‘𝑦) = (𝑓‘𝑧)) |
71 | 70 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → ((𝑓‘𝑥) ∈ (𝑓‘𝑦) ↔ (𝑓‘𝑥) ∈ (𝑓‘𝑧))) |
72 | 71 | raleqbi1dv 3123 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (∀𝑥 ∈ 𝑦 (𝑓‘𝑥) ∈ (𝑓‘𝑦) ↔ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧))) |
73 | 69, 72 | syl5bb 271 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → (∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧))) |
74 | 73 | cbvrabv 3172 |
. . . . . . . . . . . . . . 15
⊢ {𝑦 ∈ 𝐵 ∣ ∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦)} = {𝑧 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧)} |
75 | 1, 74 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ 𝐶 = {𝑧 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧)} |
76 | 66, 75 | elrab2 3333 |
. . . . . . . . . . . . 13
⊢ ((𝑂‘𝑠) ∈ 𝐶 ↔ ((𝑂‘𝑠) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)))) |
77 | 76 | simprbi 479 |
. . . . . . . . . . . 12
⊢ ((𝑂‘𝑠) ∈ 𝐶 → ∀𝑥 ∈ (𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠))) |
78 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑂‘𝑡) → (𝑓‘𝑥) = (𝑓‘(𝑂‘𝑡))) |
79 | 78 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑂‘𝑡) → ((𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)) ↔ (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠)))) |
80 | 79 | rspccv 3279 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)) → ((𝑂‘𝑡) ∈ (𝑂‘𝑠) → (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠)))) |
81 | 77, 80 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑂‘𝑠) ∈ 𝐶 → ((𝑂‘𝑡) ∈ (𝑂‘𝑠) → (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠)))) |
82 | 58, 63, 81 | sylc 63 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠))) |
83 | 21 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → 𝑂:dom 𝑂⟶𝐵) |
84 | | ordtr1 5684 |
. . . . . . . . . . . . . 14
⊢ (Ord dom
𝑂 → ((𝑡 ∈ 𝑠 ∧ 𝑠 ∈ dom 𝑂) → 𝑡 ∈ dom 𝑂)) |
85 | 84 | ancomsd 469 |
. . . . . . . . . . . . 13
⊢ (Ord dom
𝑂 → ((𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠) → 𝑡 ∈ dom 𝑂)) |
86 | 24, 26, 85 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → ((𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠) → 𝑡 ∈ dom 𝑂)) |
87 | 86 | imp 444 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → 𝑡 ∈ dom 𝑂) |
88 | | fvco3 6185 |
. . . . . . . . . . 11
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ 𝑡 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑡) = (𝑓‘(𝑂‘𝑡))) |
89 | 83, 87, 88 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → ((𝑓 ∘ 𝑂)‘𝑡) = (𝑓‘(𝑂‘𝑡))) |
90 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → 𝑠 ∈ dom 𝑂) |
91 | | fvco3 6185 |
. . . . . . . . . . 11
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ 𝑠 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑠) = (𝑓‘(𝑂‘𝑠))) |
92 | 83, 90, 91 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → ((𝑓 ∘ 𝑂)‘𝑠) = (𝑓‘(𝑂‘𝑠))) |
93 | 82, 89, 92 | 3eltr4d 2703 |
. . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠)) |
94 | 93 | ralrimivva 2954 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → ∀𝑠 ∈ dom 𝑂∀𝑡 ∈ 𝑠 ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠)) |
95 | | issmo2 7333 |
. . . . . . . . 9
⊢ ((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 → ((𝐴 ⊆ On ∧ Ord dom 𝑂 ∧ ∀𝑠 ∈ dom 𝑂∀𝑡 ∈ 𝑠 ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠)) → Smo (𝑓 ∘ 𝑂))) |
96 | 95 | imp 444 |
. . . . . . . 8
⊢ (((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ (𝐴 ⊆ On ∧ Ord dom 𝑂 ∧ ∀𝑠 ∈ dom 𝑂∀𝑡 ∈ 𝑠 ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠))) → Smo (𝑓 ∘ 𝑂)) |
97 | 51, 53, 54, 94, 96 | syl13anc 1320 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Smo (𝑓 ∘ 𝑂)) |
98 | 97 | adantrr 749 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → Smo (𝑓 ∘ 𝑂)) |
99 | 17 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → 𝑂:dom 𝑂–onto→𝐶) |
100 | | rabn0 3912 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅ ↔ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) |
101 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ 𝐵 |
102 | 101, 6 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ On → {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On) |
103 | | cofsmo.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐾 = ∩
{𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} |
104 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑤 → (𝑓‘𝑥) = (𝑓‘𝑤)) |
105 | 104 | sseq2d 3596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → (𝑧 ⊆ (𝑓‘𝑥) ↔ 𝑧 ⊆ (𝑓‘𝑤))) |
106 | 105 | cbvrabv 3172 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} = {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} |
107 | 106 | inteqi 4414 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∩ {𝑥
∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} = ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} |
108 | 103, 107 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐾 = ∩
{𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} |
109 | | onint 6887 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On ∧ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅) → ∩ {𝑤
∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
110 | 108, 109 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . 19
⊢ (({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On ∧ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅) → 𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
111 | 102, 110 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ On ∧ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅) → 𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
112 | 100, 111 | sylan2br 492 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ On ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → 𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
113 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝐾 → (𝑓‘𝑤) = (𝑓‘𝐾)) |
114 | 113 | sseq2d 3596 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝐾 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝑓‘𝐾))) |
115 | 114 | elrab 3331 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) |
116 | 112, 115 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ On ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) |
117 | 116 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ On → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)))) |
118 | 117 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)))) |
119 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . 18
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → 𝐾 ∈ 𝐵) |
120 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑤 ∈ 𝐾) |
121 | 108 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ 𝐾 ↔ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
122 | | simp21 1087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑓:𝐵⟶𝐴) |
123 | | simp1l 1078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → Ord 𝐴) |
124 | 123, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝐴 ⊆ On) |
125 | 122, 124 | fssd 5970 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑓:𝐵⟶On) |
126 | | simp22 1088 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝐾 ∈ 𝐵) |
127 | 125, 126 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑓‘𝐾) ∈ On) |
128 | | simp1r 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝐵 ∈ On) |
129 | | ontr1 5688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐵 ∈ On → ((𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) → 𝑤 ∈ 𝐵)) |
130 | 129 | 3impib 1254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) → 𝑤 ∈ 𝐵) |
131 | 128, 120,
126, 130 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑤 ∈ 𝐵) |
132 | 125, 131 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑓‘𝑤) ∈ On) |
133 | | ontri1 5674 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓‘𝐾) ∈ On ∧ (𝑓‘𝑤) ∈ On) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) ↔ ¬ (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
134 | 127, 132,
133 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) ↔ ¬ (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
135 | | simp23 1089 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑧 ⊆ (𝑓‘𝐾)) |
136 | | simpl1 1057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → 𝐵 ∈ On) |
137 | 136, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On) |
138 | | sstr 3576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤)) → 𝑧 ⊆ (𝑓‘𝑤)) |
139 | 130, 138 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → (𝑤 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝑤))) |
140 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ (𝑤 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝑤))) |
141 | 139, 140 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → 𝑤 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
142 | | onnmin 6895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On ∧ 𝑤 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
143 | 137, 141,
142 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
144 | 143 | expr 641 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ 𝑧 ⊆ (𝑓‘𝐾)) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
145 | 128, 120,
126, 135, 144 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
146 | 134, 145 | sylbird 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (¬ (𝑓‘𝑤) ∈ (𝑓‘𝐾) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
147 | 146 | con4d 113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
148 | 121, 147 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑤 ∈ 𝐾 → (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
149 | 120, 148 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑓‘𝑤) ∈ (𝑓‘𝐾)) |
150 | 149 | 3expia 1259 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → (𝑤 ∈ 𝐾 → (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
151 | 150 | ralrimiv 2948 |
. . . . . . . . . . . . . . . . . 18
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → ∀𝑤 ∈ 𝐾 (𝑓‘𝑤) ∈ (𝑓‘𝐾)) |
152 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝐾 → (𝑓‘𝑦) = (𝑓‘𝐾)) |
153 | 152 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝐾 → ((𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
154 | 153 | raleqbi1dv 3123 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝐾 → (∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ ∀𝑤 ∈ 𝐾 (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
155 | 154, 1 | elrab2 3333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ 𝐶 ↔ (𝐾 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝐾 (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
156 | 119, 151,
155 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → 𝐾 ∈ 𝐶) |
157 | 156 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) → ((Ord 𝐴 ∧ 𝐵 ∈ On) → 𝐾 ∈ 𝐶)) |
158 | 157 | 3expib 1260 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵⟶𝐴 → ((𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) → ((Ord 𝐴 ∧ 𝐵 ∈ On) → 𝐾 ∈ 𝐶))) |
159 | 158 | com13 86 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → ((𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) → (𝑓:𝐵⟶𝐴 → 𝐾 ∈ 𝐶))) |
160 | 118, 159 | syld 46 |
. . . . . . . . . . . . 13
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → (𝑓:𝐵⟶𝐴 → 𝐾 ∈ 𝐶))) |
161 | 160 | com23 84 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (𝑓:𝐵⟶𝐴 → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → 𝐾 ∈ 𝐶))) |
162 | 161 | imp31 447 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → 𝐾 ∈ 𝐶) |
163 | | foelrn 6286 |
. . . . . . . . . . 11
⊢ ((𝑂:dom 𝑂–onto→𝐶 ∧ 𝐾 ∈ 𝐶) → ∃𝑣 ∈ dom 𝑂 𝐾 = (𝑂‘𝑣)) |
164 | 99, 162, 163 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑣 ∈ dom 𝑂 𝐾 = (𝑂‘𝑣)) |
165 | | simpllr 795 |
. . . . . . . . . . . . . 14
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → 𝐵 ∈ On) |
166 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 = (𝑂‘𝑣) → (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ (𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
167 | 166 | biimpcd 238 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → (𝐾 = (𝑂‘𝑣) → (𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
168 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑂‘𝑣) → (𝑓‘𝑥) = (𝑓‘(𝑂‘𝑣))) |
169 | 168 | sseq2d 3596 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑂‘𝑣) → (𝑧 ⊆ (𝑓‘𝑥) ↔ 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
170 | 67 | sseq2d 3596 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑥 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝑓‘𝑥))) |
171 | 170 | cbvrabv 3172 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} = {𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} |
172 | 169, 171 | elrab2 3333 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ ((𝑂‘𝑣) ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
173 | 172 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣))) |
174 | 167, 173 | syl6 34 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
175 | 112, 174 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
176 | 165, 175 | sylancom 698 |
. . . . . . . . . . . . 13
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
177 | 176 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
178 | 21 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → 𝑂:dom 𝑂⟶𝐵) |
179 | | fvco3 6185 |
. . . . . . . . . . . . . 14
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ 𝑣 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑣) = (𝑓‘(𝑂‘𝑣))) |
180 | 178, 179 | sylancom 698 |
. . . . . . . . . . . . 13
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑣) = (𝑓‘(𝑂‘𝑣))) |
181 | 180 | sseq2d 3596 |
. . . . . . . . . . . 12
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → (𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣) ↔ 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
182 | 177, 181 | sylibrd 248 |
. . . . . . . . . . 11
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
183 | 182 | reximdva 3000 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (∃𝑣 ∈ dom 𝑂 𝐾 = (𝑂‘𝑣) → ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
184 | 164, 183 | mpd 15 |
. . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)) |
185 | 184 | ex 449 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
186 | 185 | ralimdv 2946 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
187 | 186 | impr 647 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)) |
188 | 49, 98, 187 | 3jca 1235 |
. . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ Smo (𝑓 ∘ 𝑂) ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
189 | | feq1 5939 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (𝑔:dom 𝑂⟶𝐴 ↔ (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴)) |
190 | | smoeq 7334 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (Smo 𝑔 ↔ Smo (𝑓 ∘ 𝑂))) |
191 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (𝑔‘𝑣) = ((𝑓 ∘ 𝑂)‘𝑣)) |
192 | 191 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (𝑧 ⊆ (𝑔‘𝑣) ↔ 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
193 | 192 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣) ↔ ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
194 | 193 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣) ↔ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
195 | 189, 190,
194 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑔 = (𝑓 ∘ 𝑂) → ((𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)) ↔ ((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ Smo (𝑓 ∘ 𝑂) ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)))) |
196 | 195 | spcegv 3267 |
. . . . 5
⊢ ((𝑓 ∘ 𝑂) ∈ V → (((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ Smo (𝑓 ∘ 𝑂) ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)) → ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)))) |
197 | 45, 188, 196 | sylc 63 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) |
198 | | feq2 5940 |
. . . . . . 7
⊢ (𝑥 = dom 𝑂 → (𝑔:𝑥⟶𝐴 ↔ 𝑔:dom 𝑂⟶𝐴)) |
199 | | rexeq 3116 |
. . . . . . . 8
⊢ (𝑥 = dom 𝑂 → (∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣) ↔ ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) |
200 | 199 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = dom 𝑂 → (∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣) ↔ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) |
201 | 198, 200 | 3anbi13d 1393 |
. . . . . 6
⊢ (𝑥 = dom 𝑂 → ((𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)) ↔ (𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)))) |
202 | 201 | exbidv 1837 |
. . . . 5
⊢ (𝑥 = dom 𝑂 → (∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)) ↔ ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)))) |
203 | 202 | rspcev 3282 |
. . . 4
⊢ ((dom
𝑂 ∈ suc 𝐵 ∧ ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣))) |
204 | 39, 197, 203 | syl2anc 691 |
. . 3
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣))) |
205 | 204 | ex 449 |
. 2
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)))) |
206 | 205 | exlimdv 1848 |
1
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)))) |