Proof of Theorem ordtypelem3
Step | Hyp | Ref
| Expression |
1 | | inss2 3796 |
. . . . 5
⊢ (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹 |
2 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑀 ∈ (𝑇 ∩ dom 𝐹)) |
3 | 1, 2 | sseldi 3566 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑀 ∈ dom 𝐹) |
4 | | ordtypelem.1 |
. . . . 5
⊢ 𝐹 = recs(𝐺) |
5 | 4 | tfr2a 7378 |
. . . 4
⊢ (𝑀 ∈ dom 𝐹 → (𝐹‘𝑀) = (𝐺‘(𝐹 ↾ 𝑀))) |
6 | 3, 5 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) = (𝐺‘(𝐹 ↾ 𝑀))) |
7 | 4 | tfr1a 7377 |
. . . . . . . . 9
⊢ (Fun
𝐹 ∧ Lim dom 𝐹) |
8 | 7 | simpri 477 |
. . . . . . . 8
⊢ Lim dom
𝐹 |
9 | | limord 5701 |
. . . . . . . 8
⊢ (Lim dom
𝐹 → Ord dom 𝐹) |
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
⊢ Ord dom
𝐹 |
11 | | ordelord 5662 |
. . . . . . 7
⊢ ((Ord dom
𝐹 ∧ 𝑀 ∈ dom 𝐹) → Ord 𝑀) |
12 | 10, 3, 11 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → Ord 𝑀) |
13 | 4 | tfr2b 7379 |
. . . . . 6
⊢ (Ord
𝑀 → (𝑀 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝑀) ∈ V)) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝑀 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝑀) ∈ V)) |
15 | 3, 14 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹 ↾ 𝑀) ∈ V) |
16 | | ordtypelem.2 |
. . . . . . 7
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} |
17 | | rneq 5272 |
. . . . . . . . . 10
⊢ (ℎ = (𝐹 ↾ 𝑀) → ran ℎ = ran (𝐹 ↾ 𝑀)) |
18 | | df-ima 5051 |
. . . . . . . . . 10
⊢ (𝐹 “ 𝑀) = ran (𝐹 ↾ 𝑀) |
19 | 17, 18 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (ℎ = (𝐹 ↾ 𝑀) → ran ℎ = (𝐹 “ 𝑀)) |
20 | 19 | raleqdv 3121 |
. . . . . . . 8
⊢ (ℎ = (𝐹 ↾ 𝑀) → (∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤)) |
21 | 20 | rabbidv 3164 |
. . . . . . 7
⊢ (ℎ = (𝐹 ↾ 𝑀) → {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}) |
22 | 16, 21 | syl5eq 2656 |
. . . . . 6
⊢ (ℎ = (𝐹 ↾ 𝑀) → 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}) |
23 | 22 | raleqdv 3121 |
. . . . . 6
⊢ (ℎ = (𝐹 ↾ 𝑀) → (∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
24 | 22, 23 | riotaeqbidv 6514 |
. . . . 5
⊢ (ℎ = (𝐹 ↾ 𝑀) → (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣) = (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
25 | | ordtypelem.3 |
. . . . 5
⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) |
26 | | riotaex 6515 |
. . . . 5
⊢
(℩𝑣
∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) ∈ V |
27 | 24, 25, 26 | fvmpt 6191 |
. . . 4
⊢ ((𝐹 ↾ 𝑀) ∈ V → (𝐺‘(𝐹 ↾ 𝑀)) = (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
28 | 15, 27 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐺‘(𝐹 ↾ 𝑀)) = (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
29 | 6, 28 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) = (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
30 | | ordtypelem.7 |
. . . . 5
⊢ (𝜑 → 𝑅 We 𝐴) |
31 | 30 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑅 We 𝐴) |
32 | | ordtypelem.8 |
. . . . 5
⊢ (𝜑 → 𝑅 Se 𝐴) |
33 | 32 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑅 Se 𝐴) |
34 | | ssrab2 3650 |
. . . . 5
⊢ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ⊆ 𝐴 |
35 | 34 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ⊆ 𝐴) |
36 | | inss1 3795 |
. . . . . . . 8
⊢ (𝑇 ∩ dom 𝐹) ⊆ 𝑇 |
37 | 36, 2 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑀 ∈ 𝑇) |
38 | | imaeq2 5381 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑀 → (𝐹 “ 𝑥) = (𝐹 “ 𝑀)) |
39 | 38 | raleqdv 3121 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑀 → (∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
40 | 39 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑥 = 𝑀 → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
41 | | ordtypelem.5 |
. . . . . . . . 9
⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} |
42 | 40, 41 | elrab2 3333 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝑇 ↔ (𝑀 ∈ On ∧ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
43 | 42 | simprbi 479 |
. . . . . . 7
⊢ (𝑀 ∈ 𝑇 → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡) |
44 | 37, 43 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡) |
45 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑗 = 𝑧 → (𝑗𝑅𝑤 ↔ 𝑧𝑅𝑤)) |
46 | 45 | cbvralv 3147 |
. . . . . . . 8
⊢
(∀𝑗 ∈
(𝐹 “ 𝑀)𝑗𝑅𝑤 ↔ ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑤) |
47 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑤 = 𝑡 → (𝑧𝑅𝑤 ↔ 𝑧𝑅𝑡)) |
48 | 47 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑤 = 𝑡 → (∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑤 ↔ ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
49 | 46, 48 | syl5bb 271 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → (∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤 ↔ ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡)) |
50 | 49 | cbvrexv 3148 |
. . . . . 6
⊢
(∃𝑤 ∈
𝐴 ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤 ↔ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑀)𝑧𝑅𝑡) |
51 | 44, 50 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → ∃𝑤 ∈ 𝐴 ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤) |
52 | | rabn0 3912 |
. . . . 5
⊢ ({𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ≠ ∅ ↔ ∃𝑤 ∈ 𝐴 ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤) |
53 | 51, 52 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ≠ ∅) |
54 | | wereu2 5035 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ ({𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ⊆ 𝐴 ∧ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ≠ ∅)) → ∃!𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) |
55 | 31, 33, 35, 53, 54 | syl22anc 1319 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → ∃!𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) |
56 | | riotacl2 6524 |
. . 3
⊢
(∃!𝑣 ∈
{𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 → (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
57 | 55, 56 | syl 17 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
58 | 29, 57 | eqeltrd 2688 |
1
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |