Metamath Proof Explorer

Theorem dfoi

Description: Rewrite df-oi with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Hypotheses dfoi.1 ⊢ C = w ∈ A | ∀ j ∈ ran ⁡ h j R w
dfoi.2 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
dfoi.3 ⊢ F = recs ⁡ G
Assertion dfoi ⊢ OrdIso R A = if R We A ∧ R Se A F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t ∅

Proof

Step Hyp Ref Expression
1 dfoi.1 ⊢ C = w ∈ A | ∀ j ∈ ran ⁡ h j R w
2 dfoi.2 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
3 dfoi.3 ⊢ F = recs ⁡ G
4 df-oi ⊢ OrdIso R A = if R We A ∧ R Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅
5 1 a1i ⊢ h ∈ V → C = w ∈ A | ∀ j ∈ ran ⁡ h j R w
6 5 raleqdv ⊢ h ∈ V → ∀ u ∈ C ¬ u R v ↔ ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
7 5 6 riotaeqbidv ⊢ h ∈ V → ι v ∈ C | ∀ u ∈ C ¬ u R v = ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
8 7 mpteq2ia ⊢ h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v = h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
9 2 8 eqtri ⊢ G = h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
10 recseq ⊢ G = h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v → recs ⁡ G = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
11 9 10 ax-mp ⊢ recs ⁡ G = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
12 3 11 eqtri ⊢ F = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
13 12 imaeq1i ⊢ F x = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x
14 13 raleqi ⊢ ∀ z ∈ F x z R t ↔ ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
15 14 rexbii ⊢ ∃ t ∈ A ∀ z ∈ F x z R t ↔ ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
16 15 rabbii ⊢ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t = x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
17 12 16 reseq12i ⊢ F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
18 ifeq1 ⊢ F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t → if R We A ∧ R Se A F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t ∅ = if R We A ∧ R Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅
19 17 18 ax-mp ⊢ if R We A ∧ R Se A F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t ∅ = if R We A ∧ R Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅
20 4 19 eqtr4i ⊢ OrdIso R A = if R We A ∧ R Se A F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t ∅