This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) = 𝐹