| Step | Hyp | Ref
| Expression |
| 1 | | noseqrdg.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 = ran 𝑅) |
| 2 | 1 | eleq2d 2827 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ 𝑆 ↔ 𝑧 ∈ ran 𝑅)) |
| 3 | | frfnom 8475 |
. . . . . . . . 9
⊢
(rec((𝑥 ∈ V,
𝑦 ∈ V ↦
〈(𝑥 +s
1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) Fn
ω |
| 4 | | noseqrdg.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)) |
| 5 | 4 | fneq1d 6661 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 Fn ω ↔ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) Fn
ω)) |
| 6 | 3, 5 | mpbiri 258 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn ω) |
| 7 | | fvelrnb 6969 |
. . . . . . . 8
⊢ (𝑅 Fn ω → (𝑧 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧)) |
| 8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧)) |
| 9 | 2, 8 | bitrd 279 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ 𝑆 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧)) |
| 10 | | om2noseq.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ No
) |
| 11 | | om2noseq.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾
ω)) |
| 12 | | om2noseq.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “
ω)) |
| 13 | | noseqrdg.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 14 | 10, 11, 12, 13, 4 | om2noseqrdg 28310 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → (𝑅‘𝑤) = 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉) |
| 15 | 10, 11, 12 | om2noseqfo 28304 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ω–onto→𝑍) |
| 16 | | fof 6820 |
. . . . . . . . . . . 12
⊢ (𝐺:ω–onto→𝑍 → 𝐺:ω⟶𝑍) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ω⟶𝑍) |
| 18 | 17 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → (𝐺‘𝑤) ∈ 𝑍) |
| 19 | | fvex 6919 |
. . . . . . . . . 10
⊢
(2nd ‘(𝑅‘𝑤)) ∈ V |
| 20 | | opelxpi 5722 |
. . . . . . . . . 10
⊢ (((𝐺‘𝑤) ∈ 𝑍 ∧ (2nd ‘(𝑅‘𝑤)) ∈ V) → 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 ∈ (𝑍 × V)) |
| 21 | 18, 19, 20 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 ∈ (𝑍 × V)) |
| 22 | 14, 21 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → (𝑅‘𝑤) ∈ (𝑍 × V)) |
| 23 | | eleq1 2829 |
. . . . . . . 8
⊢ ((𝑅‘𝑤) = 𝑧 → ((𝑅‘𝑤) ∈ (𝑍 × V) ↔ 𝑧 ∈ (𝑍 × V))) |
| 24 | 22, 23 | syl5ibcom 245 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝑅‘𝑤) = 𝑧 → 𝑧 ∈ (𝑍 × V))) |
| 25 | 24 | rexlimdva 3155 |
. . . . . 6
⊢ (𝜑 → (∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧 → 𝑧 ∈ (𝑍 × V))) |
| 26 | 9, 25 | sylbid 240 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ 𝑆 → 𝑧 ∈ (𝑍 × V))) |
| 27 | 26 | ssrdv 3989 |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ (𝑍 × V)) |
| 28 | | relxp 5703 |
. . . 4
⊢ Rel
(𝑍 ×
V) |
| 29 | | relss 5791 |
. . . 4
⊢ (𝑆 ⊆ (𝑍 × V) → (Rel (𝑍 × V) → Rel 𝑆)) |
| 30 | 27, 28, 29 | mpisyl 21 |
. . 3
⊢ (𝜑 → Rel 𝑆) |
| 31 | 1 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (〈𝑣, 𝑧〉 ∈ 𝑆 ↔ 〈𝑣, 𝑧〉 ∈ ran 𝑅)) |
| 32 | | fvelrnb 6969 |
. . . . . . . . 9
⊢ (𝑅 Fn ω → (〈𝑣, 𝑧〉 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) |
| 33 | 6, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (〈𝑣, 𝑧〉 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) |
| 34 | 31, 33 | bitrd 279 |
. . . . . . 7
⊢ (𝜑 → (〈𝑣, 𝑧〉 ∈ 𝑆 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) |
| 35 | 14 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 ↔ 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 = 〈𝑣, 𝑧〉)) |
| 36 | 35 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 = 〈𝑣, 𝑧〉)) |
| 37 | 36 | impr 454 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) → 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 = 〈𝑣, 𝑧〉) |
| 38 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢ (𝐺‘𝑤) ∈ V |
| 39 | 38, 19 | opth1 5480 |
. . . . . . . . . . . . 13
⊢
(〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 = 〈𝑣, 𝑧〉 → (𝐺‘𝑤) = 𝑣) |
| 40 | 37, 39 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) → (𝐺‘𝑤) = 𝑣) |
| 41 | 10, 11, 12 | om2noseqf1o 28307 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:ω–1-1-onto→𝑍) |
| 42 | | f1ocnvfv 7298 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:ω–1-1-onto→𝑍 ∧ 𝑤 ∈ ω) → ((𝐺‘𝑤) = 𝑣 → (◡𝐺‘𝑣) = 𝑤)) |
| 43 | 41, 42 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝐺‘𝑤) = 𝑣 → (◡𝐺‘𝑣) = 𝑤)) |
| 44 | 43 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) → ((𝐺‘𝑤) = 𝑣 → (◡𝐺‘𝑣) = 𝑤)) |
| 45 | 40, 44 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) → (◡𝐺‘𝑣) = 𝑤) |
| 46 | 45 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) → (𝑅‘(◡𝐺‘𝑣)) = (𝑅‘𝑤)) |
| 47 | 46 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) → (2nd ‘(𝑅‘(◡𝐺‘𝑣))) = (2nd ‘(𝑅‘𝑤))) |
| 48 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑣 ∈ V |
| 49 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
| 50 | 48, 49 | op2ndd 8025 |
. . . . . . . . . 10
⊢ ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → (2nd ‘(𝑅‘𝑤)) = 𝑧) |
| 51 | 50 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) → (2nd ‘(𝑅‘𝑤)) = 𝑧) |
| 52 | 47, 51 | eqtr2d 2778 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))) |
| 53 | 52 | rexlimdvaa 3156 |
. . . . . . 7
⊢ (𝜑 → (∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
| 54 | 34, 53 | sylbid 240 |
. . . . . 6
⊢ (𝜑 → (〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
| 55 | 54 | alrimiv 1927 |
. . . . 5
⊢ (𝜑 → ∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
| 56 | | fvex 6919 |
. . . . . 6
⊢
(2nd ‘(𝑅‘(◡𝐺‘𝑣))) ∈ V |
| 57 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))) → (𝑧 = 𝑤 ↔ 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
| 58 | 57 | imbi2d 340 |
. . . . . . 7
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))) → ((〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤) ↔ (〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))))) |
| 59 | 58 | albidv 1920 |
. . . . . 6
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))) → (∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤) ↔ ∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))))) |
| 60 | 56, 59 | spcev 3606 |
. . . . 5
⊢
(∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))) → ∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤)) |
| 61 | 55, 60 | syl 17 |
. . . 4
⊢ (𝜑 → ∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤)) |
| 62 | 61 | alrimiv 1927 |
. . 3
⊢ (𝜑 → ∀𝑣∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤)) |
| 63 | | dffun5 6578 |
. . 3
⊢ (Fun
𝑆 ↔ (Rel 𝑆 ∧ ∀𝑣∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤))) |
| 64 | 30, 62, 63 | sylanbrc 583 |
. 2
⊢ (𝜑 → Fun 𝑆) |
| 65 | | dmss 5913 |
. . . . 5
⊢ (𝑆 ⊆ (𝑍 × V) → dom 𝑆 ⊆ dom (𝑍 × V)) |
| 66 | 27, 65 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝑆 ⊆ dom (𝑍 × V)) |
| 67 | | dmxpss 6191 |
. . . 4
⊢ dom
(𝑍 × V) ⊆ 𝑍 |
| 68 | 66, 67 | sstrdi 3996 |
. . 3
⊢ (𝜑 → dom 𝑆 ⊆ 𝑍) |
| 69 | 10, 11, 12, 13, 4 | noseqrdglem 28311 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑍) → 〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ ran 𝑅) |
| 70 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑍) → 𝑆 = ran 𝑅) |
| 71 | 69, 70 | eleqtrrd 2844 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑍) → 〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ 𝑆) |
| 72 | 48, 56 | opeldm 5918 |
. . . 4
⊢
(〈𝑣,
(2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ 𝑆 → 𝑣 ∈ dom 𝑆) |
| 73 | 71, 72 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑍) → 𝑣 ∈ dom 𝑆) |
| 74 | 68, 73 | eqelssd 4005 |
. 2
⊢ (𝜑 → dom 𝑆 = 𝑍) |
| 75 | | df-fn 6564 |
. 2
⊢ (𝑆 Fn 𝑍 ↔ (Fun 𝑆 ∧ dom 𝑆 = 𝑍)) |
| 76 | 64, 74, 75 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑆 Fn 𝑍) |