Metamath Proof Explorer

Theorem ordtypelem3

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Hypotheses ordtypelem.1 ⊢ 𝐹 = recs ( 𝐺 )
ordtypelem.2 ⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
ordtypelem.3 ⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
ordtypelem.5 ⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
ordtypelem.6 ⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
ordtypelem.7 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
ordtypelem.8 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
Assertion ordtypelem3 ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )

Proof

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 𝐹 ) ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )