Metamath Proof Explorer


Theorem ordtypecbv

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

Ref Expression
Hypotheses ordtypelem.1 𝐹 = recs ( 𝐺 )
ordtypelem.2 𝐶 = { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 }
ordtypelem.3 𝐺 = ( ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑅 𝑣 ) )
Assertion ordtypecbv recs ( ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) = 𝐹

Proof

Step Hyp Ref Expression
1 ordtypelem.1 𝐹 = recs ( 𝐺 )
2 ordtypelem.2 𝐶 = { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 }
3 ordtypelem.3 𝐺 = ( ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑅 𝑣 ) )
4 breq1 ( 𝑢 = 𝑟 → ( 𝑢 𝑅 𝑣𝑟 𝑅 𝑣 ) )
5 4 notbid ( 𝑢 = 𝑟 → ( ¬ 𝑢 𝑅 𝑣 ↔ ¬ 𝑟 𝑅 𝑣 ) )
6 5 cbvralvw ( ∀ 𝑢𝐶 ¬ 𝑢 𝑅 𝑣 ↔ ∀ 𝑟𝐶 ¬ 𝑟 𝑅 𝑣 )
7 breq2 ( 𝑣 = 𝑠 → ( 𝑟 𝑅 𝑣𝑟 𝑅 𝑠 ) )
8 7 notbid ( 𝑣 = 𝑠 → ( ¬ 𝑟 𝑅 𝑣 ↔ ¬ 𝑟 𝑅 𝑠 ) )
9 8 ralbidv ( 𝑣 = 𝑠 → ( ∀ 𝑟𝐶 ¬ 𝑟 𝑅 𝑣 ↔ ∀ 𝑟𝐶 ¬ 𝑟 𝑅 𝑠 ) )
10 6 9 bitrid ( 𝑣 = 𝑠 → ( ∀ 𝑢𝐶 ¬ 𝑢 𝑅 𝑣 ↔ ∀ 𝑟𝐶 ¬ 𝑟 𝑅 𝑠 ) )
11 10 cbvriotavw ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑅 𝑣 ) = ( 𝑠𝐶𝑟𝐶 ¬ 𝑟 𝑅 𝑠 )
12 breq1 ( 𝑗 = 𝑖 → ( 𝑗 𝑅 𝑤𝑖 𝑅 𝑤 ) )
13 12 cbvralvw ( ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 ↔ ∀ 𝑖 ∈ ran 𝑖 𝑅 𝑤 )
14 breq2 ( 𝑤 = 𝑦 → ( 𝑖 𝑅 𝑤𝑖 𝑅 𝑦 ) )
15 14 ralbidv ( 𝑤 = 𝑦 → ( ∀ 𝑖 ∈ ran 𝑖 𝑅 𝑤 ↔ ∀ 𝑖 ∈ ran 𝑖 𝑅 𝑦 ) )
16 13 15 bitrid ( 𝑤 = 𝑦 → ( ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 ↔ ∀ 𝑖 ∈ ran 𝑖 𝑅 𝑦 ) )
17 16 cbvrabv { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } = { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑖 𝑅 𝑦 }
18 2 17 eqtri 𝐶 = { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑖 𝑅 𝑦 }
19 rneq ( = 𝑓 → ran = ran 𝑓 )
20 19 raleqdv ( = 𝑓 → ( ∀ 𝑖 ∈ ran 𝑖 𝑅 𝑦 ↔ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 ) )
21 20 rabbidv ( = 𝑓 → { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑖 𝑅 𝑦 } = { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } )
22 18 21 eqtrid ( = 𝑓𝐶 = { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } )
23 22 raleqdv ( = 𝑓 → ( ∀ 𝑟𝐶 ¬ 𝑟 𝑅 𝑠 ↔ ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
24 22 23 riotaeqbidv ( = 𝑓 → ( 𝑠𝐶𝑟𝐶 ¬ 𝑟 𝑅 𝑠 ) = ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
25 11 24 eqtrid ( = 𝑓 → ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑅 𝑣 ) = ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
26 25 cbvmptv ( ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑅 𝑣 ) ) = ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
27 3 26 eqtri 𝐺 = ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
28 recseq ( 𝐺 = ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) → recs ( 𝐺 ) = recs ( ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) )
29 27 28 ax-mp recs ( 𝐺 ) = recs ( ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) )
30 1 29 eqtr2i recs ( ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) = 𝐹