Step | Hyp | Ref
| Expression |
1 | | cofsmo.1 |
. . . . . . . . . . . . 13
⊢ 𝐶 = {𝑦 ∈ 𝐵 ∣ ∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦)} |
2 | 1 | ssrab3 4057 |
. . . . . . . . . . . 12
⊢ 𝐶 ⊆ 𝐵 |
3 | | ssexg 5220 |
. . . . . . . . . . . 12
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ On) → 𝐶 ∈ V) |
4 | 2, 3 | mpan 688 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → 𝐶 ∈ V) |
5 | | onss 7499 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) |
6 | 2, 5 | sstrid 3978 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ On → 𝐶 ⊆ On) |
7 | | epweon 7491 |
. . . . . . . . . . . 12
⊢ E We
On |
8 | | wess 5537 |
. . . . . . . . . . . 12
⊢ (𝐶 ⊆ On → ( E We On
→ E We 𝐶)) |
9 | 6, 7, 8 | mpisyl 21 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → E We 𝐶) |
10 | | cofsmo.3 |
. . . . . . . . . . . 12
⊢ 𝑂 = OrdIso( E , 𝐶) |
11 | 10 | oiiso 8995 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ V ∧ E We 𝐶) → 𝑂 Isom E , E (dom 𝑂, 𝐶)) |
12 | 4, 9, 11 | syl2anc 586 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → 𝑂 Isom E , E (dom 𝑂, 𝐶)) |
13 | 12 | ad2antlr 725 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂 Isom E , E (dom 𝑂, 𝐶)) |
14 | | isof1o 7070 |
. . . . . . . . 9
⊢ (𝑂 Isom E , E (dom 𝑂, 𝐶) → 𝑂:dom 𝑂–1-1-onto→𝐶) |
15 | | f1ofo 6617 |
. . . . . . . . 9
⊢ (𝑂:dom 𝑂–1-1-onto→𝐶 → 𝑂:dom 𝑂–onto→𝐶) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂:dom 𝑂–onto→𝐶) |
17 | | fof 6585 |
. . . . . . . . 9
⊢ (𝑂:dom 𝑂–onto→𝐶 → 𝑂:dom 𝑂⟶𝐶) |
18 | | fss 6522 |
. . . . . . . . 9
⊢ ((𝑂:dom 𝑂⟶𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝑂:dom 𝑂⟶𝐵) |
19 | 17, 2, 18 | sylancl 588 |
. . . . . . . 8
⊢ (𝑂:dom 𝑂–onto→𝐶 → 𝑂:dom 𝑂⟶𝐵) |
20 | 16, 19 | syl 17 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂:dom 𝑂⟶𝐵) |
21 | 10 | oion 8994 |
. . . . . . . . . 10
⊢ (𝐶 ∈ V → dom 𝑂 ∈ On) |
22 | 4, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → dom 𝑂 ∈ On) |
23 | 22 | ad2antlr 725 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → dom 𝑂 ∈ On) |
24 | | simplr 767 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝐵 ∈ On) |
25 | | eloni 6196 |
. . . . . . . . . . 11
⊢ (dom
𝑂 ∈ On → Ord dom
𝑂) |
26 | | smoiso2 8000 |
. . . . . . . . . . 11
⊢ ((Ord dom
𝑂 ∧ 𝐶 ⊆ On) → ((𝑂:dom 𝑂–onto→𝐶 ∧ Smo 𝑂) ↔ 𝑂 Isom E , E (dom 𝑂, 𝐶))) |
27 | 25, 6, 26 | syl2an 597 |
. . . . . . . . . 10
⊢ ((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) → ((𝑂:dom 𝑂–onto→𝐶 ∧ Smo 𝑂) ↔ 𝑂 Isom E , E (dom 𝑂, 𝐶))) |
28 | 27 | biimpar 480 |
. . . . . . . . 9
⊢ (((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑂 Isom E , E (dom 𝑂, 𝐶)) → (𝑂:dom 𝑂–onto→𝐶 ∧ Smo 𝑂)) |
29 | 28 | simprd 498 |
. . . . . . . 8
⊢ (((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑂 Isom E , E (dom 𝑂, 𝐶)) → Smo 𝑂) |
30 | 23, 24, 13, 29 | syl21anc 835 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Smo 𝑂) |
31 | | eloni 6196 |
. . . . . . . 8
⊢ (𝐵 ∈ On → Ord 𝐵) |
32 | 31 | ad2antlr 725 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Ord 𝐵) |
33 | | smorndom 7999 |
. . . . . . 7
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ Smo 𝑂 ∧ Ord 𝐵) → dom 𝑂 ⊆ 𝐵) |
34 | 20, 30, 32, 33 | syl3anc 1367 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → dom 𝑂 ⊆ 𝐵) |
35 | | onsssuc 6273 |
. . . . . . 7
⊢ ((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) → (dom 𝑂 ⊆ 𝐵 ↔ dom 𝑂 ∈ suc 𝐵)) |
36 | 23, 24, 35 | syl2anc 586 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (dom 𝑂 ⊆ 𝐵 ↔ dom 𝑂 ∈ suc 𝐵)) |
37 | 34, 36 | mpbid 234 |
. . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → dom 𝑂 ∈ suc 𝐵) |
38 | 37 | adantrr 715 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → dom 𝑂 ∈ suc 𝐵) |
39 | | vex 3498 |
. . . . . 6
⊢ 𝑓 ∈ V |
40 | 10 | oiexg 8993 |
. . . . . . . 8
⊢ (𝐶 ∈ V → 𝑂 ∈ V) |
41 | 4, 40 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ On → 𝑂 ∈ V) |
42 | 41 | ad2antlr 725 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → 𝑂 ∈ V) |
43 | | coexg 7628 |
. . . . . 6
⊢ ((𝑓 ∈ V ∧ 𝑂 ∈ V) → (𝑓 ∘ 𝑂) ∈ V) |
44 | 39, 42, 43 | sylancr 589 |
. . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (𝑓 ∘ 𝑂) ∈ V) |
45 | | simprl 769 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → 𝑓:𝐵⟶𝐴) |
46 | 20 | adantrr 715 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → 𝑂:dom 𝑂⟶𝐵) |
47 | | fco 6526 |
. . . . . . 7
⊢ ((𝑓:𝐵⟶𝐴 ∧ 𝑂:dom 𝑂⟶𝐵) → (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴) |
48 | 45, 46, 47 | syl2anc 586 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴) |
49 | | simpr 487 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑓:𝐵⟶𝐴) |
50 | 49, 20, 47 | syl2anc 586 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴) |
51 | | ordsson 7498 |
. . . . . . . . 9
⊢ (Ord
𝐴 → 𝐴 ⊆ On) |
52 | 51 | ad2antrr 724 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝐴 ⊆ On) |
53 | 23, 25 | syl 17 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Ord dom 𝑂) |
54 | 16, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂:dom 𝑂⟶𝐶) |
55 | | simpl 485 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠) → 𝑠 ∈ dom 𝑂) |
56 | | ffvelrn 6844 |
. . . . . . . . . . . 12
⊢ ((𝑂:dom 𝑂⟶𝐶 ∧ 𝑠 ∈ dom 𝑂) → (𝑂‘𝑠) ∈ 𝐶) |
57 | 54, 55, 56 | syl2an 597 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑂‘𝑠) ∈ 𝐶) |
58 | | ffn 6509 |
. . . . . . . . . . . . . 14
⊢ (𝑂:dom 𝑂⟶𝐶 → 𝑂 Fn dom 𝑂) |
59 | 16, 17, 58 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂 Fn dom 𝑂) |
60 | 59, 30 | jca 514 |
. . . . . . . . . . . 12
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (𝑂 Fn dom 𝑂 ∧ Smo 𝑂)) |
61 | | smoel2 7994 |
. . . . . . . . . . . 12
⊢ (((𝑂 Fn dom 𝑂 ∧ Smo 𝑂) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑂‘𝑡) ∈ (𝑂‘𝑠)) |
62 | 60, 61 | sylan 582 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑂‘𝑡) ∈ (𝑂‘𝑠)) |
63 | | fveq2 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑂‘𝑠) → (𝑓‘𝑧) = (𝑓‘(𝑂‘𝑠))) |
64 | 63 | eleq2d 2898 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑂‘𝑠) → ((𝑓‘𝑥) ∈ (𝑓‘𝑧) ↔ (𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)))) |
65 | 64 | raleqbi1dv 3404 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑂‘𝑠) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧) ↔ ∀𝑥 ∈ (𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)))) |
66 | | fveq2 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑥 → (𝑓‘𝑤) = (𝑓‘𝑥)) |
67 | 66 | eleq1d 2897 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → ((𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ (𝑓‘𝑥) ∈ (𝑓‘𝑦))) |
68 | 67 | cbvralvw 3450 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑤 ∈
𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) ∈ (𝑓‘𝑦)) |
69 | | fveq2 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → (𝑓‘𝑦) = (𝑓‘𝑧)) |
70 | 69 | eleq2d 2898 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → ((𝑓‘𝑥) ∈ (𝑓‘𝑦) ↔ (𝑓‘𝑥) ∈ (𝑓‘𝑧))) |
71 | 70 | raleqbi1dv 3404 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (∀𝑥 ∈ 𝑦 (𝑓‘𝑥) ∈ (𝑓‘𝑦) ↔ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧))) |
72 | 68, 71 | syl5bb 285 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → (∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧))) |
73 | 72 | cbvrabv 3492 |
. . . . . . . . . . . . . . 15
⊢ {𝑦 ∈ 𝐵 ∣ ∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦)} = {𝑧 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧)} |
74 | 1, 73 | eqtri 2844 |
. . . . . . . . . . . . . 14
⊢ 𝐶 = {𝑧 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧)} |
75 | 65, 74 | elrab2 3683 |
. . . . . . . . . . . . 13
⊢ ((𝑂‘𝑠) ∈ 𝐶 ↔ ((𝑂‘𝑠) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)))) |
76 | 75 | simprbi 499 |
. . . . . . . . . . . 12
⊢ ((𝑂‘𝑠) ∈ 𝐶 → ∀𝑥 ∈ (𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠))) |
77 | | fveq2 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑂‘𝑡) → (𝑓‘𝑥) = (𝑓‘(𝑂‘𝑡))) |
78 | 77 | eleq1d 2897 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑂‘𝑡) → ((𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)) ↔ (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠)))) |
79 | 78 | rspccv 3620 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)) → ((𝑂‘𝑡) ∈ (𝑂‘𝑠) → (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠)))) |
80 | 76, 79 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑂‘𝑠) ∈ 𝐶 → ((𝑂‘𝑡) ∈ (𝑂‘𝑠) → (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠)))) |
81 | 57, 62, 80 | sylc 65 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠))) |
82 | | ordtr1 6229 |
. . . . . . . . . . . . . 14
⊢ (Ord dom
𝑂 → ((𝑡 ∈ 𝑠 ∧ 𝑠 ∈ dom 𝑂) → 𝑡 ∈ dom 𝑂)) |
83 | 82 | ancomsd 468 |
. . . . . . . . . . . . 13
⊢ (Ord dom
𝑂 → ((𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠) → 𝑡 ∈ dom 𝑂)) |
84 | 23, 25, 83 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → ((𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠) → 𝑡 ∈ dom 𝑂)) |
85 | 84 | imp 409 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → 𝑡 ∈ dom 𝑂) |
86 | | fvco3 6755 |
. . . . . . . . . . 11
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ 𝑡 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑡) = (𝑓‘(𝑂‘𝑡))) |
87 | 20, 85, 86 | syl2an2r 683 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → ((𝑓 ∘ 𝑂)‘𝑡) = (𝑓‘(𝑂‘𝑡))) |
88 | | simprl 769 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → 𝑠 ∈ dom 𝑂) |
89 | | fvco3 6755 |
. . . . . . . . . . 11
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ 𝑠 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑠) = (𝑓‘(𝑂‘𝑠))) |
90 | 20, 88, 89 | syl2an2r 683 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → ((𝑓 ∘ 𝑂)‘𝑠) = (𝑓‘(𝑂‘𝑠))) |
91 | 81, 87, 90 | 3eltr4d 2928 |
. . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠)) |
92 | 91 | ralrimivva 3191 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → ∀𝑠 ∈ dom 𝑂∀𝑡 ∈ 𝑠 ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠)) |
93 | | issmo2 7980 |
. . . . . . . . 9
⊢ ((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 → ((𝐴 ⊆ On ∧ Ord dom 𝑂 ∧ ∀𝑠 ∈ dom 𝑂∀𝑡 ∈ 𝑠 ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠)) → Smo (𝑓 ∘ 𝑂))) |
94 | 93 | imp 409 |
. . . . . . . 8
⊢ (((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ (𝐴 ⊆ On ∧ Ord dom 𝑂 ∧ ∀𝑠 ∈ dom 𝑂∀𝑡 ∈ 𝑠 ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠))) → Smo (𝑓 ∘ 𝑂)) |
95 | 50, 52, 53, 92, 94 | syl13anc 1368 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Smo (𝑓 ∘ 𝑂)) |
96 | 95 | adantrr 715 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → Smo (𝑓 ∘ 𝑂)) |
97 | | rabn0 4339 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅ ↔ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) |
98 | | ssrab2 4056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ 𝐵 |
99 | 98, 5 | sstrid 3978 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ On → {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On) |
100 | | cofsmo.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐾 = ∩
{𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} |
101 | | fveq2 6665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑤 → (𝑓‘𝑥) = (𝑓‘𝑤)) |
102 | 101 | sseq2d 3999 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → (𝑧 ⊆ (𝑓‘𝑥) ↔ 𝑧 ⊆ (𝑓‘𝑤))) |
103 | 102 | cbvrabv 3492 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} = {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} |
104 | 103 | inteqi 4873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∩ {𝑥
∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} = ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} |
105 | 100, 104 | eqtri 2844 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐾 = ∩
{𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} |
106 | | onint 7504 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On ∧ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅) → ∩ {𝑤
∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
107 | 105, 106 | eqeltrid 2917 |
. . . . . . . . . . . . . . . . . . 19
⊢ (({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On ∧ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅) → 𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
108 | 99, 107 | sylan 582 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ On ∧ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅) → 𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
109 | 97, 108 | sylan2br 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ On ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → 𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
110 | | fveq2 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝐾 → (𝑓‘𝑤) = (𝑓‘𝐾)) |
111 | 110 | sseq2d 3999 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝐾 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝑓‘𝐾))) |
112 | 111 | elrab 3680 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) |
113 | 109, 112 | sylib 220 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ On ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) |
114 | 113 | ex 415 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ On → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)))) |
115 | 114 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)))) |
116 | | simpr2 1191 |
. . . . . . . . . . . . . . . . . 18
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → 𝐾 ∈ 𝐵) |
117 | | simp3 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑤 ∈ 𝐾) |
118 | 105 | eleq2i 2904 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ 𝐾 ↔ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
119 | | simp21 1202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑓:𝐵⟶𝐴) |
120 | | simp1l 1193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → Ord 𝐴) |
121 | 120, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝐴 ⊆ On) |
122 | 119, 121 | fssd 6523 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑓:𝐵⟶On) |
123 | | simp22 1203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝐾 ∈ 𝐵) |
124 | 122, 123 | ffvelrnd 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑓‘𝐾) ∈ On) |
125 | | simp1r 1194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝐵 ∈ On) |
126 | | ontr1 6232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐵 ∈ On → ((𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) → 𝑤 ∈ 𝐵)) |
127 | 126 | 3impib 1112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) → 𝑤 ∈ 𝐵) |
128 | 125, 117,
123, 127 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑤 ∈ 𝐵) |
129 | 122, 128 | ffvelrnd 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑓‘𝑤) ∈ On) |
130 | | ontri1 6220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓‘𝐾) ∈ On ∧ (𝑓‘𝑤) ∈ On) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) ↔ ¬ (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
131 | 124, 129,
130 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) ↔ ¬ (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
132 | | simp23 1204 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑧 ⊆ (𝑓‘𝐾)) |
133 | | simpl1 1187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → 𝐵 ∈ On) |
134 | 133, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On) |
135 | | sstr 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤)) → 𝑧 ⊆ (𝑓‘𝑤)) |
136 | 127, 135 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → (𝑤 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝑤))) |
137 | | rabid 3379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ (𝑤 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝑤))) |
138 | 136, 137 | sylibr 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → 𝑤 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
139 | | onnmin 7512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On ∧ 𝑤 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
140 | 134, 138,
139 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) |
141 | 140 | expr 459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ 𝑧 ⊆ (𝑓‘𝐾)) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
142 | 125, 117,
123, 132, 141 | syl31anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
143 | 131, 142 | sylbird 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (¬ (𝑓‘𝑤) ∈ (𝑓‘𝐾) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
144 | 143 | con4d 115 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
145 | 118, 144 | syl5bi 244 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑤 ∈ 𝐾 → (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
146 | 117, 145 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑓‘𝑤) ∈ (𝑓‘𝐾)) |
147 | 146 | 3expia 1117 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → (𝑤 ∈ 𝐾 → (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
148 | 147 | ralrimiv 3181 |
. . . . . . . . . . . . . . . . . 18
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → ∀𝑤 ∈ 𝐾 (𝑓‘𝑤) ∈ (𝑓‘𝐾)) |
149 | | fveq2 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝐾 → (𝑓‘𝑦) = (𝑓‘𝐾)) |
150 | 149 | eleq2d 2898 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝐾 → ((𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
151 | 150 | raleqbi1dv 3404 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝐾 → (∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ ∀𝑤 ∈ 𝐾 (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
152 | 151, 1 | elrab2 3683 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ 𝐶 ↔ (𝐾 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝐾 (𝑓‘𝑤) ∈ (𝑓‘𝐾))) |
153 | 116, 148,
152 | sylanbrc 585 |
. . . . . . . . . . . . . . . . 17
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → 𝐾 ∈ 𝐶) |
154 | 153 | expcom 416 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) → ((Ord 𝐴 ∧ 𝐵 ∈ On) → 𝐾 ∈ 𝐶)) |
155 | 154 | 3expib 1118 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵⟶𝐴 → ((𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) → ((Ord 𝐴 ∧ 𝐵 ∈ On) → 𝐾 ∈ 𝐶))) |
156 | 155 | com13 88 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → ((𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) → (𝑓:𝐵⟶𝐴 → 𝐾 ∈ 𝐶))) |
157 | 115, 156 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → (𝑓:𝐵⟶𝐴 → 𝐾 ∈ 𝐶))) |
158 | 157 | com23 86 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (𝑓:𝐵⟶𝐴 → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → 𝐾 ∈ 𝐶))) |
159 | 158 | imp31 420 |
. . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → 𝐾 ∈ 𝐶) |
160 | | foelrn 6867 |
. . . . . . . . . . 11
⊢ ((𝑂:dom 𝑂–onto→𝐶 ∧ 𝐾 ∈ 𝐶) → ∃𝑣 ∈ dom 𝑂 𝐾 = (𝑂‘𝑣)) |
161 | 16, 159, 160 | syl2an2r 683 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑣 ∈ dom 𝑂 𝐾 = (𝑂‘𝑣)) |
162 | | eleq1 2900 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 = (𝑂‘𝑣) → (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ (𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
163 | 162 | biimpcd 251 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → (𝐾 = (𝑂‘𝑣) → (𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) |
164 | | fveq2 6665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑂‘𝑣) → (𝑓‘𝑥) = (𝑓‘(𝑂‘𝑣))) |
165 | 164 | sseq2d 3999 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑂‘𝑣) → (𝑧 ⊆ (𝑓‘𝑥) ↔ 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
166 | 66 | sseq2d 3999 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝑓‘𝑥))) |
167 | 166 | cbvrabv 3492 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} = {𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} |
168 | 165, 167 | elrab2 3683 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ ((𝑂‘𝑣) ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
169 | 168 | simprbi 499 |
. . . . . . . . . . . . . . 15
⊢ ((𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣))) |
170 | 163, 169 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
171 | 109, 170 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
172 | 171 | ad5ant24 759 |
. . . . . . . . . . . 12
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
173 | 20 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → 𝑂:dom 𝑂⟶𝐵) |
174 | | fvco3 6755 |
. . . . . . . . . . . . . 14
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ 𝑣 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑣) = (𝑓‘(𝑂‘𝑣))) |
175 | 173, 174 | sylancom 590 |
. . . . . . . . . . . . 13
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑣) = (𝑓‘(𝑂‘𝑣))) |
176 | 175 | sseq2d 3999 |
. . . . . . . . . . . 12
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → (𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣) ↔ 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) |
177 | 172, 176 | sylibrd 261 |
. . . . . . . . . . 11
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
178 | 177 | reximdva 3274 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (∃𝑣 ∈ dom 𝑂 𝐾 = (𝑂‘𝑣) → ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
179 | 161, 178 | mpd 15 |
. . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)) |
180 | 179 | ex 415 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
181 | 180 | ralimdv 3178 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
182 | 181 | impr 457 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)) |
183 | 48, 96, 182 | 3jca 1124 |
. . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ Smo (𝑓 ∘ 𝑂) ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
184 | | feq1 6490 |
. . . . . 6
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (𝑔:dom 𝑂⟶𝐴 ↔ (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴)) |
185 | | smoeq 7981 |
. . . . . 6
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (Smo 𝑔 ↔ Smo (𝑓 ∘ 𝑂))) |
186 | | fveq1 6664 |
. . . . . . . . 9
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (𝑔‘𝑣) = ((𝑓 ∘ 𝑂)‘𝑣)) |
187 | 186 | sseq2d 3999 |
. . . . . . . 8
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (𝑧 ⊆ (𝑔‘𝑣) ↔ 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
188 | 187 | rexbidv 3297 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣) ↔ ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
189 | 188 | ralbidv 3197 |
. . . . . 6
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣) ↔ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) |
190 | 184, 185,
189 | 3anbi123d 1432 |
. . . . 5
⊢ (𝑔 = (𝑓 ∘ 𝑂) → ((𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)) ↔ ((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ Smo (𝑓 ∘ 𝑂) ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)))) |
191 | 44, 183, 190 | spcedv 3599 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) |
192 | | feq2 6491 |
. . . . . . 7
⊢ (𝑥 = dom 𝑂 → (𝑔:𝑥⟶𝐴 ↔ 𝑔:dom 𝑂⟶𝐴)) |
193 | | rexeq 3407 |
. . . . . . . 8
⊢ (𝑥 = dom 𝑂 → (∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣) ↔ ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) |
194 | 193 | ralbidv 3197 |
. . . . . . 7
⊢ (𝑥 = dom 𝑂 → (∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣) ↔ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) |
195 | 192, 194 | 3anbi13d 1434 |
. . . . . 6
⊢ (𝑥 = dom 𝑂 → ((𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)) ↔ (𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)))) |
196 | 195 | exbidv 1918 |
. . . . 5
⊢ (𝑥 = dom 𝑂 → (∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)) ↔ ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)))) |
197 | 196 | rspcev 3623 |
. . . 4
⊢ ((dom
𝑂 ∈ suc 𝐵 ∧ ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣))) |
198 | 38, 191, 197 | syl2anc 586 |
. . 3
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣))) |
199 | 198 | ex 415 |
. 2
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)))) |
200 | 199 | exlimdv 1930 |
1
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)))) |