Step |
Hyp |
Ref |
Expression |
1 |
|
ordtypelem.1 |
⊢ 𝐹 = recs ( 𝐺 ) |
2 |
|
ordtypelem.2 |
⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 } |
3 |
|
ordtypelem.3 |
⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) ) |
4 |
|
ordtypelem.5 |
⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } |
5 |
|
ordtypelem.6 |
⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 ) |
6 |
|
ordtypelem.7 |
⊢ ( 𝜑 → 𝑅 We 𝐴 ) |
7 |
|
ordtypelem.8 |
⊢ ( 𝜑 → 𝑅 Se 𝐴 ) |
8 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) |
9 |
8
|
elin2d |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → 𝑀 ∈ dom 𝐹 ) |
10 |
1
|
tfr2a |
⊢ ( 𝑀 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑀 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑀 ) ) ) |
11 |
9 10
|
syl |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑀 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑀 ) ) ) |
12 |
1
|
tfr1a |
⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 ) |
13 |
12
|
simpri |
⊢ Lim dom 𝐹 |
14 |
|
limord |
⊢ ( Lim dom 𝐹 → Ord dom 𝐹 ) |
15 |
13 14
|
ax-mp |
⊢ Ord dom 𝐹 |
16 |
|
ordelord |
⊢ ( ( Ord dom 𝐹 ∧ 𝑀 ∈ dom 𝐹 ) → Ord 𝑀 ) |
17 |
15 9 16
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → Ord 𝑀 ) |
18 |
1
|
tfr2b |
⊢ ( Ord 𝑀 → ( 𝑀 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝑀 ) ∈ V ) ) |
19 |
17 18
|
syl |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝑀 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝑀 ) ∈ V ) ) |
20 |
9 19
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ↾ 𝑀 ) ∈ V ) |
21 |
|
rneq |
⊢ ( ℎ = ( 𝐹 ↾ 𝑀 ) → ran ℎ = ran ( 𝐹 ↾ 𝑀 ) ) |
22 |
|
df-ima |
⊢ ( 𝐹 “ 𝑀 ) = ran ( 𝐹 ↾ 𝑀 ) |
23 |
21 22
|
eqtr4di |
⊢ ( ℎ = ( 𝐹 ↾ 𝑀 ) → ran ℎ = ( 𝐹 “ 𝑀 ) ) |
24 |
23
|
raleqdv |
⊢ ( ℎ = ( 𝐹 ↾ 𝑀 ) → ( ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 ↔ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 ) ) |
25 |
24
|
rabbidv |
⊢ ( ℎ = ( 𝐹 ↾ 𝑀 ) → { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 } = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ) |
26 |
2 25
|
eqtrid |
⊢ ( ℎ = ( 𝐹 ↾ 𝑀 ) → 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ) |
27 |
26
|
raleqdv |
⊢ ( ℎ = ( 𝐹 ↾ 𝑀 ) → ( ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ↔ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) |
28 |
26 27
|
riotaeqbidv |
⊢ ( ℎ = ( 𝐹 ↾ 𝑀 ) → ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) = ( ℩ 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) |
29 |
|
riotaex |
⊢ ( ℩ 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ∈ V |
30 |
28 3 29
|
fvmpt |
⊢ ( ( 𝐹 ↾ 𝑀 ) ∈ V → ( 𝐺 ‘ ( 𝐹 ↾ 𝑀 ) ) = ( ℩ 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) |
31 |
20 30
|
syl |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐺 ‘ ( 𝐹 ↾ 𝑀 ) ) = ( ℩ 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) |
32 |
11 31
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑀 ) = ( ℩ 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) |
33 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → 𝑅 We 𝐴 ) |
34 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → 𝑅 Se 𝐴 ) |
35 |
|
ssrab2 |
⊢ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ⊆ 𝐴 |
36 |
35
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ⊆ 𝐴 ) |
37 |
8
|
elin1d |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → 𝑀 ∈ 𝑇 ) |
38 |
|
imaeq2 |
⊢ ( 𝑥 = 𝑀 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑀 ) ) |
39 |
38
|
raleqdv |
⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑡 ) ) |
40 |
39
|
rexbidv |
⊢ ( 𝑥 = 𝑀 → ( ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑡 ) ) |
41 |
40 4
|
elrab2 |
⊢ ( 𝑀 ∈ 𝑇 ↔ ( 𝑀 ∈ On ∧ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑡 ) ) |
42 |
41
|
simprbi |
⊢ ( 𝑀 ∈ 𝑇 → ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑡 ) |
43 |
37 42
|
syl |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑡 ) |
44 |
|
breq1 |
⊢ ( 𝑗 = 𝑧 → ( 𝑗 𝑅 𝑤 ↔ 𝑧 𝑅 𝑤 ) ) |
45 |
44
|
cbvralvw |
⊢ ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 ↔ ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑤 ) |
46 |
|
breq2 |
⊢ ( 𝑤 = 𝑡 → ( 𝑧 𝑅 𝑤 ↔ 𝑧 𝑅 𝑡 ) ) |
47 |
46
|
ralbidv |
⊢ ( 𝑤 = 𝑡 → ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑤 ↔ ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑡 ) ) |
48 |
45 47
|
syl5bb |
⊢ ( 𝑤 = 𝑡 → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 ↔ ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑡 ) ) |
49 |
48
|
cbvrexvw |
⊢ ( ∃ 𝑤 ∈ 𝐴 ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 ↔ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑀 ) 𝑧 𝑅 𝑡 ) |
50 |
43 49
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ∃ 𝑤 ∈ 𝐴 ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 ) |
51 |
|
rabn0 |
⊢ ( { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ≠ ∅ ↔ ∃ 𝑤 ∈ 𝐴 ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 ) |
52 |
50 51
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ≠ ∅ ) |
53 |
|
wereu2 |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ⊆ 𝐴 ∧ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ≠ ∅ ) ) → ∃! 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) |
54 |
33 34 36 52 53
|
syl22anc |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ∃! 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) |
55 |
|
riotacl2 |
⊢ ( ∃! 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 → ( ℩ 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ) |
56 |
54 55
|
syl |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( ℩ 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ) |
57 |
32 56
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ) |