Metamath Proof Explorer

Theorem nfoi

Description: Hypothesis builder for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses nfoi.1 ⊢ Ⅎ _ x R
nfoi.2 ⊢ Ⅎ _ x A
Assertion nfoi ⊢ Ⅎ _ x OrdIso R A

Proof

Step Hyp Ref Expression
1 nfoi.1 ⊢ Ⅎ _ x R
2 nfoi.2 ⊢ Ⅎ _ x A
3 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 ↾ a ∈ 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 a z R t ∅
4 1 2 nfwe ⊢ Ⅎ x R We A
5 1 2 nfse ⊢ Ⅎ x R Se A
6 4 5 nfan ⊢ Ⅎ x R We A ∧ R Se A
7 nfcv ⊢ Ⅎ _ x V
8 nfcv ⊢ Ⅎ _ x ran ⁡ h
9 nfcv ⊢ Ⅎ _ x j
10 nfcv ⊢ Ⅎ _ x w
11 9 1 10 nfbr ⊢ Ⅎ x j R w
12 8 11 nfralw ⊢ Ⅎ x ∀ j ∈ ran ⁡ h j R w
13 12 2 nfrabw ⊢ Ⅎ _ x w ∈ A | ∀ j ∈ ran ⁡ h j R w
14 nfcv ⊢ Ⅎ _ x u
15 nfcv ⊢ Ⅎ _ x v
16 14 1 15 nfbr ⊢ Ⅎ x u R v
17 16 nfn ⊢ Ⅎ x ¬ u R v
18 13 17 nfralw ⊢ Ⅎ x ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
19 18 13 nfriota ⊢ Ⅎ _ x ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
20 7 19 nfmpt ⊢ Ⅎ _ x h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
21 20 nfrecs ⊢ Ⅎ _ 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
22 nfcv ⊢ Ⅎ _ x a
23 21 22 nfima ⊢ Ⅎ _ 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 a
24 nfcv ⊢ Ⅎ _ x z
25 nfcv ⊢ Ⅎ _ x t
26 24 1 25 nfbr ⊢ Ⅎ x z R t
27 23 26 nfralw ⊢ Ⅎ x ∀ 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 a z R t
28 2 27 nfrex ⊢ Ⅎ x ∃ 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 a z R t
29 nfcv ⊢ Ⅎ _ x On
30 28 29 nfrabw ⊢ Ⅎ _ x a ∈ 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 a z R t
31 21 30 nfres ⊢ Ⅎ _ 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 ↾ a ∈ 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 a z R t
32 nfcv ⊢ Ⅎ _ x ∅
33 6 31 32 nfif ⊢ Ⅎ _ x 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 ↾ a ∈ 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 a z R t ∅
34 3 33 nfcxfr ⊢ Ⅎ _ x OrdIso R A