| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cofsmo.1 | . . . . . . . . . . . . 13
⊢ 𝐶 = {𝑦 ∈ 𝐵 ∣ ∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦)} | 
| 2 | 1 | ssrab3 4081 | . . . . . . . . . . . 12
⊢ 𝐶 ⊆ 𝐵 | 
| 3 |  | ssexg 5322 | . . . . . . . . . . . 12
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ On) → 𝐶 ∈ V) | 
| 4 | 2, 3 | mpan 690 | . . . . . . . . . . 11
⊢ (𝐵 ∈ On → 𝐶 ∈ V) | 
| 5 |  | onss 7806 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) | 
| 6 | 2, 5 | sstrid 3994 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ On → 𝐶 ⊆ On) | 
| 7 |  | epweon 7796 | . . . . . . . . . . . 12
⊢  E We
On | 
| 8 |  | wess 5670 | . . . . . . . . . . . 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 9578 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ V ∧ E We 𝐶) → 𝑂 Isom E , E (dom 𝑂, 𝐶)) | 
| 12 | 4, 9, 11 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝐵 ∈ On → 𝑂 Isom E , E (dom 𝑂, 𝐶)) | 
| 13 | 12 | ad2antlr 727 | . . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂 Isom E , E (dom 𝑂, 𝐶)) | 
| 14 |  | isof1o 7344 | . . . . . . . . 9
⊢ (𝑂 Isom E , E (dom 𝑂, 𝐶) → 𝑂:dom 𝑂–1-1-onto→𝐶) | 
| 15 |  | f1ofo 6854 | . . . . . . . . 9
⊢ (𝑂:dom 𝑂–1-1-onto→𝐶 → 𝑂:dom 𝑂–onto→𝐶) | 
| 16 | 13, 14, 15 | 3syl 18 | . . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂:dom 𝑂–onto→𝐶) | 
| 17 |  | fof 6819 | . . . . . . . . 9
⊢ (𝑂:dom 𝑂–onto→𝐶 → 𝑂:dom 𝑂⟶𝐶) | 
| 18 |  | fss 6751 | . . . . . . . . 9
⊢ ((𝑂:dom 𝑂⟶𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝑂:dom 𝑂⟶𝐵) | 
| 19 | 17, 2, 18 | sylancl 586 | . . . . . . . 8
⊢ (𝑂:dom 𝑂–onto→𝐶 → 𝑂:dom 𝑂⟶𝐵) | 
| 20 | 16, 19 | syl 17 | . . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂:dom 𝑂⟶𝐵) | 
| 21 | 10 | oion 9577 | . . . . . . . . . 10
⊢ (𝐶 ∈ V → dom 𝑂 ∈ On) | 
| 22 | 4, 21 | syl 17 | . . . . . . . . 9
⊢ (𝐵 ∈ On → dom 𝑂 ∈ On) | 
| 23 | 22 | ad2antlr 727 | . . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → dom 𝑂 ∈ On) | 
| 24 |  | simplr 768 | . . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝐵 ∈ On) | 
| 25 |  | eloni 6393 | . . . . . . . . . . 11
⊢ (dom
𝑂 ∈ On → Ord dom
𝑂) | 
| 26 |  | smoiso2 8410 | . . . . . . . . . . 11
⊢ ((Ord dom
𝑂 ∧ 𝐶 ⊆ On) → ((𝑂:dom 𝑂–onto→𝐶 ∧ Smo 𝑂) ↔ 𝑂 Isom E , E (dom 𝑂, 𝐶))) | 
| 27 | 25, 6, 26 | syl2an 596 | . . . . . . . . . 10
⊢ ((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) → ((𝑂:dom 𝑂–onto→𝐶 ∧ Smo 𝑂) ↔ 𝑂 Isom E , E (dom 𝑂, 𝐶))) | 
| 28 | 27 | biimpar 477 | . . . . . . . . 9
⊢ (((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑂 Isom E , E (dom 𝑂, 𝐶)) → (𝑂:dom 𝑂–onto→𝐶 ∧ Smo 𝑂)) | 
| 29 | 28 | simprd 495 | . . . . . . . 8
⊢ (((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑂 Isom E , E (dom 𝑂, 𝐶)) → Smo 𝑂) | 
| 30 | 23, 24, 13, 29 | syl21anc 837 | . . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Smo 𝑂) | 
| 31 |  | eloni 6393 | . . . . . . . 8
⊢ (𝐵 ∈ On → Ord 𝐵) | 
| 32 | 31 | ad2antlr 727 | . . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Ord 𝐵) | 
| 33 |  | smocdmdom 8409 | . . . . . . 7
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ Smo 𝑂 ∧ Ord 𝐵) → dom 𝑂 ⊆ 𝐵) | 
| 34 | 20, 30, 32, 33 | syl3anc 1372 | . . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → dom 𝑂 ⊆ 𝐵) | 
| 35 |  | onsssuc 6473 | . . . . . . 7
⊢ ((dom
𝑂 ∈ On ∧ 𝐵 ∈ On) → (dom 𝑂 ⊆ 𝐵 ↔ dom 𝑂 ∈ suc 𝐵)) | 
| 36 | 23, 24, 35 | syl2anc 584 | . . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (dom 𝑂 ⊆ 𝐵 ↔ dom 𝑂 ∈ suc 𝐵)) | 
| 37 | 34, 36 | mpbid 232 | . . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → dom 𝑂 ∈ suc 𝐵) | 
| 38 | 37 | adantrr 717 | . . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → dom 𝑂 ∈ suc 𝐵) | 
| 39 |  | vex 3483 | . . . . . 6
⊢ 𝑓 ∈ V | 
| 40 | 10 | oiexg 9576 | . . . . . . . 8
⊢ (𝐶 ∈ V → 𝑂 ∈ V) | 
| 41 | 4, 40 | syl 17 | . . . . . . 7
⊢ (𝐵 ∈ On → 𝑂 ∈ V) | 
| 42 | 41 | ad2antlr 727 | . . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → 𝑂 ∈ V) | 
| 43 |  | coexg 7952 | . . . . . 6
⊢ ((𝑓 ∈ V ∧ 𝑂 ∈ V) → (𝑓 ∘ 𝑂) ∈ V) | 
| 44 | 39, 42, 43 | sylancr 587 | . . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (𝑓 ∘ 𝑂) ∈ V) | 
| 45 |  | simprl 770 | . . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → 𝑓:𝐵⟶𝐴) | 
| 46 | 20 | adantrr 717 | . . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → 𝑂:dom 𝑂⟶𝐵) | 
| 47 | 45, 46 | fcod 6760 | . . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴) | 
| 48 |  | simpr 484 | . . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑓:𝐵⟶𝐴) | 
| 49 | 48, 20 | fcod 6760 | . . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴) | 
| 50 |  | ordsson 7804 | . . . . . . . . 9
⊢ (Ord
𝐴 → 𝐴 ⊆ On) | 
| 51 | 50 | ad2antrr 726 | . . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝐴 ⊆ On) | 
| 52 | 23, 25 | syl 17 | . . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Ord dom 𝑂) | 
| 53 | 16, 17 | syl 17 | . . . . . . . . . . . 12
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂:dom 𝑂⟶𝐶) | 
| 54 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠) → 𝑠 ∈ dom 𝑂) | 
| 55 |  | ffvelcdm 7100 | . . . . . . . . . . . 12
⊢ ((𝑂:dom 𝑂⟶𝐶 ∧ 𝑠 ∈ dom 𝑂) → (𝑂‘𝑠) ∈ 𝐶) | 
| 56 | 53, 54, 55 | syl2an 596 | . . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑂‘𝑠) ∈ 𝐶) | 
| 57 |  | ffn 6735 | . . . . . . . . . . . . . 14
⊢ (𝑂:dom 𝑂⟶𝐶 → 𝑂 Fn dom 𝑂) | 
| 58 | 16, 17, 57 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → 𝑂 Fn dom 𝑂) | 
| 59 | 58, 30 | jca 511 | . . . . . . . . . . . 12
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (𝑂 Fn dom 𝑂 ∧ Smo 𝑂)) | 
| 60 |  | smoel2 8404 | . . . . . . . . . . . 12
⊢ (((𝑂 Fn dom 𝑂 ∧ Smo 𝑂) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑂‘𝑡) ∈ (𝑂‘𝑠)) | 
| 61 | 59, 60 | sylan 580 | . . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑂‘𝑡) ∈ (𝑂‘𝑠)) | 
| 62 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑂‘𝑠) → (𝑓‘𝑧) = (𝑓‘(𝑂‘𝑠))) | 
| 63 | 62 | eleq2d 2826 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑂‘𝑠) → ((𝑓‘𝑥) ∈ (𝑓‘𝑧) ↔ (𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)))) | 
| 64 | 63 | raleqbi1dv 3337 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑂‘𝑠) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧) ↔ ∀𝑥 ∈ (𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)))) | 
| 65 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑥 → (𝑓‘𝑤) = (𝑓‘𝑥)) | 
| 66 | 65 | eleq1d 2825 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → ((𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ (𝑓‘𝑥) ∈ (𝑓‘𝑦))) | 
| 67 | 66 | cbvralvw 3236 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑤 ∈
𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) ∈ (𝑓‘𝑦)) | 
| 68 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → (𝑓‘𝑦) = (𝑓‘𝑧)) | 
| 69 | 68 | eleq2d 2826 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → ((𝑓‘𝑥) ∈ (𝑓‘𝑦) ↔ (𝑓‘𝑥) ∈ (𝑓‘𝑧))) | 
| 70 | 69 | raleqbi1dv 3337 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (∀𝑥 ∈ 𝑦 (𝑓‘𝑥) ∈ (𝑓‘𝑦) ↔ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧))) | 
| 71 | 67, 70 | bitrid 283 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → (∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧))) | 
| 72 | 71 | cbvrabv 3446 | . . . . . . . . . . . . . . 15
⊢ {𝑦 ∈ 𝐵 ∣ ∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦)} = {𝑧 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧)} | 
| 73 | 1, 72 | eqtri 2764 | . . . . . . . . . . . . . 14
⊢ 𝐶 = {𝑧 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ (𝑓‘𝑧)} | 
| 74 | 64, 73 | elrab2 3694 | . . . . . . . . . . . . 13
⊢ ((𝑂‘𝑠) ∈ 𝐶 ↔ ((𝑂‘𝑠) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)))) | 
| 75 | 74 | simprbi 496 | . . . . . . . . . . . 12
⊢ ((𝑂‘𝑠) ∈ 𝐶 → ∀𝑥 ∈ (𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠))) | 
| 76 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑂‘𝑡) → (𝑓‘𝑥) = (𝑓‘(𝑂‘𝑡))) | 
| 77 | 76 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝑂‘𝑡) → ((𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)) ↔ (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠)))) | 
| 78 | 77 | rspccv 3618 | . . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝑂‘𝑠)(𝑓‘𝑥) ∈ (𝑓‘(𝑂‘𝑠)) → ((𝑂‘𝑡) ∈ (𝑂‘𝑠) → (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠)))) | 
| 79 | 75, 78 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑂‘𝑠) ∈ 𝐶 → ((𝑂‘𝑡) ∈ (𝑂‘𝑠) → (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠)))) | 
| 80 | 56, 61, 79 | sylc 65 | . . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → (𝑓‘(𝑂‘𝑡)) ∈ (𝑓‘(𝑂‘𝑠))) | 
| 81 |  | ordtr1 6426 | . . . . . . . . . . . . . 14
⊢ (Ord dom
𝑂 → ((𝑡 ∈ 𝑠 ∧ 𝑠 ∈ dom 𝑂) → 𝑡 ∈ dom 𝑂)) | 
| 82 | 81 | ancomsd 465 | . . . . . . . . . . . . 13
⊢ (Ord dom
𝑂 → ((𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠) → 𝑡 ∈ dom 𝑂)) | 
| 83 | 23, 25, 82 | 3syl 18 | . . . . . . . . . . . 12
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → ((𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠) → 𝑡 ∈ dom 𝑂)) | 
| 84 | 83 | imp 406 | . . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → 𝑡 ∈ dom 𝑂) | 
| 85 |  | fvco3 7007 | . . . . . . . . . . 11
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ 𝑡 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑡) = (𝑓‘(𝑂‘𝑡))) | 
| 86 | 20, 84, 85 | syl2an2r 685 | . . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → ((𝑓 ∘ 𝑂)‘𝑡) = (𝑓‘(𝑂‘𝑡))) | 
| 87 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → 𝑠 ∈ dom 𝑂) | 
| 88 |  | fvco3 7007 | . . . . . . . . . . 11
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ 𝑠 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑠) = (𝑓‘(𝑂‘𝑠))) | 
| 89 | 20, 87, 88 | syl2an2r 685 | . . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → ((𝑓 ∘ 𝑂)‘𝑠) = (𝑓‘(𝑂‘𝑠))) | 
| 90 | 80, 86, 89 | 3eltr4d 2855 | . . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ (𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠)) → ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠)) | 
| 91 | 90 | ralrimivva 3201 | . . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → ∀𝑠 ∈ dom 𝑂∀𝑡 ∈ 𝑠 ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠)) | 
| 92 |  | issmo2 8390 | . . . . . . . . 9
⊢ ((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 → ((𝐴 ⊆ On ∧ Ord dom 𝑂 ∧ ∀𝑠 ∈ dom 𝑂∀𝑡 ∈ 𝑠 ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠)) → Smo (𝑓 ∘ 𝑂))) | 
| 93 | 92 | imp 406 | . . . . . . . 8
⊢ (((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ (𝐴 ⊆ On ∧ Ord dom 𝑂 ∧ ∀𝑠 ∈ dom 𝑂∀𝑡 ∈ 𝑠 ((𝑓 ∘ 𝑂)‘𝑡) ∈ ((𝑓 ∘ 𝑂)‘𝑠))) → Smo (𝑓 ∘ 𝑂)) | 
| 94 | 49, 51, 52, 91, 93 | syl13anc 1373 | . . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → Smo (𝑓 ∘ 𝑂)) | 
| 95 | 94 | adantrr 717 | . . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → Smo (𝑓 ∘ 𝑂)) | 
| 96 |  | rabn0 4388 | . . . . . . . . . . . . . . . . . 18
⊢ ({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅ ↔ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) | 
| 97 |  | ssrab2 4079 | . . . . . . . . . . . . . . . . . . . 20
⊢ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ 𝐵 | 
| 98 | 97, 5 | sstrid 3994 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ On → {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On) | 
| 99 |  | cofsmo.2 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐾 = ∩
{𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} | 
| 100 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑤 → (𝑓‘𝑥) = (𝑓‘𝑤)) | 
| 101 | 100 | sseq2d 4015 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → (𝑧 ⊆ (𝑓‘𝑥) ↔ 𝑧 ⊆ (𝑓‘𝑤))) | 
| 102 | 101 | cbvrabv 3446 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ {𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} = {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} | 
| 103 | 102 | inteqi 4949 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ∩ {𝑥
∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} = ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} | 
| 104 | 99, 103 | eqtri 2764 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝐾 = ∩
{𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} | 
| 105 |  | onint 7811 | . . . . . . . . . . . . . . . . . . . 20
⊢ (({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On ∧ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅) → ∩ {𝑤
∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) | 
| 106 | 104, 105 | eqeltrid 2844 | . . . . . . . . . . . . . . . . . . 19
⊢ (({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On ∧ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅) → 𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) | 
| 107 | 98, 106 | sylan 580 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ On ∧ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ≠ ∅) → 𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) | 
| 108 | 96, 107 | sylan2br 595 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ On ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → 𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) | 
| 109 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝐾 → (𝑓‘𝑤) = (𝑓‘𝐾)) | 
| 110 | 109 | sseq2d 4015 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝐾 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝑓‘𝐾))) | 
| 111 | 110 | elrab 3691 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) | 
| 112 | 108, 111 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ On ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) | 
| 113 | 112 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ On → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)))) | 
| 114 | 113 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → (𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)))) | 
| 115 |  | simpr2 1195 | . . . . . . . . . . . . . . . . . 18
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → 𝐾 ∈ 𝐵) | 
| 116 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑤 ∈ 𝐾) | 
| 117 | 104 | eleq2i 2832 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ 𝐾 ↔ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) | 
| 118 |  | simp21 1206 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑓:𝐵⟶𝐴) | 
| 119 |  | simp1l 1197 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → Ord 𝐴) | 
| 120 | 119, 50 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝐴 ⊆ On) | 
| 121 | 118, 120 | fssd 6752 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑓:𝐵⟶On) | 
| 122 |  | simp22 1207 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝐾 ∈ 𝐵) | 
| 123 | 121, 122 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑓‘𝐾) ∈ On) | 
| 124 |  | simp1r 1198 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝐵 ∈ On) | 
| 125 |  | ontr1 6429 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐵 ∈ On → ((𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) → 𝑤 ∈ 𝐵)) | 
| 126 | 125 | 3impib 1116 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) → 𝑤 ∈ 𝐵) | 
| 127 | 124, 116,
122, 126 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑤 ∈ 𝐵) | 
| 128 | 121, 127 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑓‘𝑤) ∈ On) | 
| 129 |  | ontri1 6417 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓‘𝐾) ∈ On ∧ (𝑓‘𝑤) ∈ On) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) ↔ ¬ (𝑓‘𝑤) ∈ (𝑓‘𝐾))) | 
| 130 | 123, 128,
129 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) ↔ ¬ (𝑓‘𝑤) ∈ (𝑓‘𝐾))) | 
| 131 |  | simp23 1208 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → 𝑧 ⊆ (𝑓‘𝐾)) | 
| 132 |  | simpl1 1191 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → 𝐵 ∈ On) | 
| 133 | 132, 98 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On) | 
| 134 |  | sstr 3991 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤)) → 𝑧 ⊆ (𝑓‘𝑤)) | 
| 135 | 126, 134 | anim12i 613 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → (𝑤 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝑤))) | 
| 136 |  | rabid 3457 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ (𝑤 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝑤))) | 
| 137 | 135, 136 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → 𝑤 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) | 
| 138 |  | onnmin 7819 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (({𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ⊆ On ∧ 𝑤 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) | 
| 139 | 133, 137,
138 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ (𝑧 ⊆ (𝑓‘𝐾) ∧ (𝑓‘𝐾) ⊆ (𝑓‘𝑤))) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)}) | 
| 140 | 139 | expr 456 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵) ∧ 𝑧 ⊆ (𝑓‘𝐾)) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) | 
| 141 | 124, 116,
122, 131, 140 | syl31anc 1374 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → ((𝑓‘𝐾) ⊆ (𝑓‘𝑤) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) | 
| 142 | 130, 141 | sylbird 260 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (¬ (𝑓‘𝑤) ∈ (𝑓‘𝐾) → ¬ 𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) | 
| 143 | 142 | con4d 115 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑤 ∈ ∩ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → (𝑓‘𝑤) ∈ (𝑓‘𝐾))) | 
| 144 | 117, 143 | biimtrid 242 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑤 ∈ 𝐾 → (𝑓‘𝑤) ∈ (𝑓‘𝐾))) | 
| 145 | 116, 144 | mpd 15 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) ∧ 𝑤 ∈ 𝐾) → (𝑓‘𝑤) ∈ (𝑓‘𝐾)) | 
| 146 | 145 | 3expia 1121 | . . . . . . . . . . . . . . . . . . 19
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → (𝑤 ∈ 𝐾 → (𝑓‘𝑤) ∈ (𝑓‘𝐾))) | 
| 147 | 146 | ralrimiv 3144 | . . . . . . . . . . . . . . . . . 18
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → ∀𝑤 ∈ 𝐾 (𝑓‘𝑤) ∈ (𝑓‘𝐾)) | 
| 148 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝐾 → (𝑓‘𝑦) = (𝑓‘𝐾)) | 
| 149 | 148 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝐾 → ((𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ (𝑓‘𝑤) ∈ (𝑓‘𝐾))) | 
| 150 | 149 | raleqbi1dv 3337 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝐾 → (∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦) ↔ ∀𝑤 ∈ 𝐾 (𝑓‘𝑤) ∈ (𝑓‘𝐾))) | 
| 151 | 150, 1 | elrab2 3694 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ 𝐶 ↔ (𝐾 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝐾 (𝑓‘𝑤) ∈ (𝑓‘𝐾))) | 
| 152 | 115, 147,
151 | sylanbrc 583 | . . . . . . . . . . . . . . . . 17
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾))) → 𝐾 ∈ 𝐶) | 
| 153 | 152 | expcom 413 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐵⟶𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) → ((Ord 𝐴 ∧ 𝐵 ∈ On) → 𝐾 ∈ 𝐶)) | 
| 154 | 153 | 3expib 1122 | . . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵⟶𝐴 → ((𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) → ((Ord 𝐴 ∧ 𝐵 ∈ On) → 𝐾 ∈ 𝐶))) | 
| 155 | 154 | com13 88 | . . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → ((𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘𝐾)) → (𝑓:𝐵⟶𝐴 → 𝐾 ∈ 𝐶))) | 
| 156 | 114, 155 | syld 47 | . . . . . . . . . . . . 13
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → (𝑓:𝐵⟶𝐴 → 𝐾 ∈ 𝐶))) | 
| 157 | 156 | com23 86 | . . . . . . . . . . . 12
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (𝑓:𝐵⟶𝐴 → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → 𝐾 ∈ 𝐶))) | 
| 158 | 157 | imp31 417 | . . . . . . . . . . 11
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → 𝐾 ∈ 𝐶) | 
| 159 |  | foelrn 7126 | . . . . . . . . . . 11
⊢ ((𝑂:dom 𝑂–onto→𝐶 ∧ 𝐾 ∈ 𝐶) → ∃𝑣 ∈ dom 𝑂 𝐾 = (𝑂‘𝑣)) | 
| 160 | 16, 158, 159 | syl2an2r 685 | . . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑣 ∈ dom 𝑂 𝐾 = (𝑂‘𝑣)) | 
| 161 |  | eleq1 2828 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 = (𝑂‘𝑣) → (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ (𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) | 
| 162 | 161 | biimpcd 249 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → (𝐾 = (𝑂‘𝑣) → (𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)})) | 
| 163 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑂‘𝑣) → (𝑓‘𝑥) = (𝑓‘(𝑂‘𝑣))) | 
| 164 | 163 | sseq2d 4015 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑂‘𝑣) → (𝑧 ⊆ (𝑓‘𝑥) ↔ 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) | 
| 165 | 65 | sseq2d 4015 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝑓‘𝑥))) | 
| 166 | 165 | cbvrabv 3446 | . . . . . . . . . . . . . . . . 17
⊢ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} = {𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} | 
| 167 | 164, 166 | elrab2 3694 | . . . . . . . . . . . . . . . 16
⊢ ((𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} ↔ ((𝑂‘𝑣) ∈ 𝐵 ∧ 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) | 
| 168 | 167 | simprbi 496 | . . . . . . . . . . . . . . 15
⊢ ((𝑂‘𝑣) ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣))) | 
| 169 | 162, 168 | syl6 35 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ {𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑤)} → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) | 
| 170 | 108, 169 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) | 
| 171 | 170 | ad5ant24 760 | . . . . . . . . . . . 12
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) | 
| 172 | 20 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → 𝑂:dom 𝑂⟶𝐵) | 
| 173 |  | fvco3 7007 | . . . . . . . . . . . . . 14
⊢ ((𝑂:dom 𝑂⟶𝐵 ∧ 𝑣 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑣) = (𝑓‘(𝑂‘𝑣))) | 
| 174 | 172, 173 | sylancom 588 | . . . . . . . . . . . . 13
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → ((𝑓 ∘ 𝑂)‘𝑣) = (𝑓‘(𝑂‘𝑣))) | 
| 175 | 174 | sseq2d 4015 | . . . . . . . . . . . 12
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → (𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣) ↔ 𝑧 ⊆ (𝑓‘(𝑂‘𝑣)))) | 
| 176 | 171, 175 | sylibrd 259 | . . . . . . . . . . 11
⊢ (((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) ∧ 𝑣 ∈ dom 𝑂) → (𝐾 = (𝑂‘𝑣) → 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) | 
| 177 | 176 | reximdva 3167 | . . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (∃𝑣 ∈ dom 𝑂 𝐾 = (𝑂‘𝑣) → ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) | 
| 178 | 160, 177 | mpd 15 | . . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)) | 
| 179 | 178 | ex 412 | . . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) | 
| 180 | 179 | ralimdv 3168 | . . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) | 
| 181 | 180 | impr 454 | . . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)) | 
| 182 | 47, 95, 181 | 3jca 1128 | . . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ Smo (𝑓 ∘ 𝑂) ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) | 
| 183 |  | feq1 6715 | . . . . . 6
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (𝑔:dom 𝑂⟶𝐴 ↔ (𝑓 ∘ 𝑂):dom 𝑂⟶𝐴)) | 
| 184 |  | smoeq 8391 | . . . . . 6
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (Smo 𝑔 ↔ Smo (𝑓 ∘ 𝑂))) | 
| 185 |  | fveq1 6904 | . . . . . . . . 9
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (𝑔‘𝑣) = ((𝑓 ∘ 𝑂)‘𝑣)) | 
| 186 | 185 | sseq2d 4015 | . . . . . . . 8
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (𝑧 ⊆ (𝑔‘𝑣) ↔ 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) | 
| 187 | 186 | rexbidv 3178 | . . . . . . 7
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣) ↔ ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) | 
| 188 | 187 | ralbidv 3177 | . . . . . 6
⊢ (𝑔 = (𝑓 ∘ 𝑂) → (∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣) ↔ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣))) | 
| 189 | 183, 184,
188 | 3anbi123d 1437 | . . . . 5
⊢ (𝑔 = (𝑓 ∘ 𝑂) → ((𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)) ↔ ((𝑓 ∘ 𝑂):dom 𝑂⟶𝐴 ∧ Smo (𝑓 ∘ 𝑂) ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ ((𝑓 ∘ 𝑂)‘𝑣)))) | 
| 190 | 44, 182, 189 | spcedv 3597 | . . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) | 
| 191 |  | feq2 6716 | . . . . . . 7
⊢ (𝑥 = dom 𝑂 → (𝑔:𝑥⟶𝐴 ↔ 𝑔:dom 𝑂⟶𝐴)) | 
| 192 |  | rexeq 3321 | . . . . . . . 8
⊢ (𝑥 = dom 𝑂 → (∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣) ↔ ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) | 
| 193 | 192 | ralbidv 3177 | . . . . . . 7
⊢ (𝑥 = dom 𝑂 → (∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣) ↔ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) | 
| 194 | 191, 193 | 3anbi13d 1439 | . . . . . 6
⊢ (𝑥 = dom 𝑂 → ((𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)) ↔ (𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)))) | 
| 195 | 194 | exbidv 1920 | . . . . 5
⊢ (𝑥 = dom 𝑂 → (∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)) ↔ ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣)))) | 
| 196 | 195 | rspcev 3621 | . . . 4
⊢ ((dom
𝑂 ∈ suc 𝐵 ∧ ∃𝑔(𝑔:dom 𝑂⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ dom 𝑂 𝑧 ⊆ (𝑔‘𝑣))) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣))) | 
| 197 | 38, 190, 196 | syl2anc 584 | . . 3
⊢ (((Ord
𝐴 ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣))) | 
| 198 | 197 | ex 412 | . 2
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)))) | 
| 199 | 198 | exlimdv 1932 | 1
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)))) |