Proof of Theorem ordtypelem3
| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑀 ∈ (𝑇 ∩ dom 𝐹)) |
| 2 | 1 | elin2d 4205 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑀 ∈ dom 𝐹) |
| 3 | | ordtypelem.1 |
. . . . 5
⊢ 𝐹 = recs(𝐺) |
| 4 | 3 | tfr2a 8435 |
. . . 4
⊢ (𝑀 ∈ dom 𝐹 → (𝐹‘𝑀) = (𝐺‘(𝐹 ↾ 𝑀))) |
| 5 | 2, 4 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) = (𝐺‘(𝐹 ↾ 𝑀))) |
| 6 | 3 | tfr1a 8434 |
. . . . . . . . 9
⊢ (Fun
𝐹 ∧ Lim dom 𝐹) |
| 7 | 6 | simpri 485 |
. . . . . . . 8
⊢ Lim dom
𝐹 |
| 8 | | limord 6444 |
. . . . . . . 8
⊢ (Lim dom
𝐹 → Ord dom 𝐹) |
| 9 | 7, 8 | ax-mp 5 |
. . . . . . 7
⊢ Ord dom
𝐹 |
| 10 | | ordelord 6406 |
. . . . . . 7
⊢ ((Ord dom
𝐹 ∧ 𝑀 ∈ dom 𝐹) → Ord 𝑀) |
| 11 | 9, 2, 10 | sylancr 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → Ord 𝑀) |
| 12 | 3 | tfr2b 8436 |
. . . . . 6
⊢ (Ord
𝑀 → (𝑀 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝑀) ∈ V)) |
| 13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝑀 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝑀) ∈ V)) |
| 14 | 2, 13 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹 ↾ 𝑀) ∈ V) |
| 15 | | ordtypelem.2 |
. . . . . . 7
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} |
| 16 | | rneq 5947 |
. . . . . . . . . 10
⊢ (ℎ = (𝐹 ↾ 𝑀) → ran ℎ = ran (𝐹 ↾ 𝑀)) |
| 17 | | df-ima 5698 |
. . . . . . . . . 10
⊢ (𝐹 “ 𝑀) = ran (𝐹 ↾ 𝑀) |
| 18 | 16, 17 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (ℎ = (𝐹 ↾ 𝑀) → ran ℎ = (𝐹 “ 𝑀)) |
| 19 | 18 | raleqdv 3326 |
. . . . . . . 8
⊢ (ℎ = (𝐹 ↾ 𝑀) → (∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤)) |
| 20 | 19 | rabbidv 3444 |
. . . . . . 7
⊢ (ℎ = (𝐹 ↾ 𝑀) → {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}) |
| 21 | 15, 20 | eqtrid 2789 |
. . . . . 6
⊢ (ℎ = (𝐹 ↾ 𝑀) → 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}) |
| 22 | 21 | raleqdv 3326 |
. . . . . 6
⊢ (ℎ = (𝐹 ↾ 𝑀) → (∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
| 23 | 21, 22 | riotaeqbidv 7391 |
. . . . 5
⊢ (ℎ = (𝐹 ↾ 𝑀) → (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣) = (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
| 24 | | ordtypelem.3 |
. . . . 5
⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) |
| 25 | | riotaex 7392 |
. . . . 5
⊢
(℩𝑣
∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) ∈ V |
| 26 | 23, 24, 25 | fvmpt 7016 |
. . . 4
⊢ ((𝐹 ↾ 𝑀) ∈ V → (𝐺‘(𝐹 ↾ 𝑀)) = (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
| 27 | 14, 26 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐺‘(𝐹 ↾ 𝑀)) = (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
| 28 | 5, 27 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) = (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
| 29 | | ordtypelem.7 |
. . . . 5
⊢ (𝜑 → 𝑅 We 𝐴) |
| 30 | 29 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑅 We 𝐴) |
| 31 | | ordtypelem.8 |
. . . . 5
⊢ (𝜑 → 𝑅 Se 𝐴) |
| 32 | 31 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑅 Se 𝐴) |
| 33 | | ssrab2 4080 |
. . . . 5
⊢ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ⊆ 𝐴 |
| 34 | 33 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ⊆ 𝐴) |
| 35 | 1 | elin1d 4204 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑀 ∈ 𝑇) |
| 36 | | imaeq2 6074 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑀 → (𝐹 “ 𝑥) = (𝐹 “ 𝑀)) |
| 37 | 36 | raleqdv 3326 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑀 → (∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
| 38 | 37 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑥 = 𝑀 → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
| 39 | | ordtypelem.5 |
. . . . . . . . 9
⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} |
| 40 | 38, 39 | elrab2 3695 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝑇 ↔ (𝑀 ∈ On ∧ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
| 41 | 40 | simprbi 496 |
. . . . . . 7
⊢ (𝑀 ∈ 𝑇 → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡) |
| 42 | 35, 41 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡) |
| 43 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑗 = 𝑧 → (𝑗𝑅𝑤 ↔ 𝑧𝑅𝑤)) |
| 44 | 43 | cbvralvw 3237 |
. . . . . . . 8
⊢
(∀𝑗 ∈
(𝐹 “ 𝑀)𝑗𝑅𝑤 ↔ ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑤) |
| 45 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑤 = 𝑡 → (𝑧𝑅𝑤 ↔ 𝑧𝑅𝑡)) |
| 46 | 45 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑤 = 𝑡 → (∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑤 ↔ ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
| 47 | 44, 46 | bitrid 283 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → (∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤 ↔ ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
| 48 | 47 | cbvrexvw 3238 |
. . . . . 6
⊢
(∃𝑤 ∈
𝐴 ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤 ↔ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡) |
| 49 | 42, 48 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → ∃𝑤 ∈ 𝐴 ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤) |
| 50 | | rabn0 4389 |
. . . . 5
⊢ ({𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ≠ ∅ ↔ ∃𝑤 ∈ 𝐴 ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤) |
| 51 | 49, 50 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ≠ ∅) |
| 52 | | wereu2 5682 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ ({𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ⊆ 𝐴 ∧ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ≠ ∅)) → ∃!𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) |
| 53 | 30, 32, 34, 51, 52 | syl22anc 839 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → ∃!𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) |
| 54 | | riotacl2 7404 |
. . 3
⊢
(∃!𝑣 ∈
{𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 → (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
| 55 | 53, 54 | syl 17 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
| 56 | 28, 55 | eqeltrd 2841 |
1
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |