Metamath Proof Explorer

Theorem ordtypecbv

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

Ref Expression
Hypotheses ordtypelem.1 ⊢ F = recs ⁡ G
ordtypelem.2 ⊢ C = w ∈ A | ∀ j ∈ ran ⁡ h j R w
ordtypelem.3 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
Assertion ordtypecbv ⊢ recs ⁡ f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s = F

Proof

Step Hyp Ref Expression
1 ordtypelem.1 ⊢ F = recs ⁡ G
2 ordtypelem.2 ⊢ C = w ∈ A | ∀ j ∈ ran ⁡ h j R w
3 ordtypelem.3 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
4 breq1 ⊢ u = r → u R v ↔ r R v
5 4 notbid ⊢ u = r → ¬ u R v ↔ ¬ r R v
6 5 cbvralvw ⊢ ∀ u ∈ C ¬ u R v ↔ ∀ r ∈ C ¬ r R v
7 breq2 ⊢ v = s → r R v ↔ r R s
8 7 notbid ⊢ v = s → ¬ r R v ↔ ¬ r R s
9 8 ralbidv ⊢ v = s → ∀ r ∈ C ¬ r R v ↔ ∀ r ∈ C ¬ r R s
10 6 9 bitrid ⊢ v = s → ∀ u ∈ C ¬ u R v ↔ ∀ r ∈ C ¬ r R s
11 10 cbvriotavw ⊢ ι v ∈ C | ∀ u ∈ C ¬ u R v = ι s ∈ C | ∀ r ∈ C ¬ r R s
12 breq1 ⊢ j = i → j R w ↔ i R w
13 12 cbvralvw ⊢ ∀ j ∈ ran ⁡ h j R w ↔ ∀ i ∈ ran ⁡ h i R w
14 breq2 ⊢ w = y → i R w ↔ i R y
15 14 ralbidv ⊢ w = y → ∀ i ∈ ran ⁡ h i R w ↔ ∀ i ∈ ran ⁡ h i R y
16 13 15 bitrid ⊢ w = y → ∀ j ∈ ran ⁡ h j R w ↔ ∀ i ∈ ran ⁡ h i R y
17 16 cbvrabv ⊢ w ∈ A | ∀ j ∈ ran ⁡ h j R w = y ∈ A | ∀ i ∈ ran ⁡ h i R y
18 2 17 eqtri ⊢ C = y ∈ A | ∀ i ∈ ran ⁡ h i R y
19 rneq ⊢ h = f → ran ⁡ h = ran ⁡ f
20 19 raleqdv ⊢ h = f → ∀ i ∈ ran ⁡ h i R y ↔ ∀ i ∈ ran ⁡ f i R y
21 20 rabbidv ⊢ h = f → y ∈ A | ∀ i ∈ ran ⁡ h i R y = y ∈ A | ∀ i ∈ ran ⁡ f i R y
22 18 21 eqtrid ⊢ h = f → C = y ∈ A | ∀ i ∈ ran ⁡ f i R y
23 22 raleqdv ⊢ h = f → ∀ r ∈ C ¬ r R s ↔ ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s
24 22 23 riotaeqbidv ⊢ h = f → ι s ∈ C | ∀ r ∈ C ¬ r R s = ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s
25 11 24 eqtrid ⊢ h = f → ι v ∈ C | ∀ u ∈ C ¬ u R v = ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s
26 25 cbvmptv ⊢ h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v = f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s
27 3 26 eqtri ⊢ G = f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s
28 recseq ⊢ G = f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s → recs ⁡ G = recs ⁡ f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s
29 27 28 ax-mp ⊢ recs ⁡ G = recs ⁡ f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s
30 1 29 eqtr2i ⊢ recs ⁡ f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s = F