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