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 𝑥 𝑅
nfoi.2 𝑥 𝐴
Assertion nfoi 𝑥 OrdIso ( 𝑅 , 𝐴 )

Proof

Step Hyp Ref Expression
1 nfoi.1 𝑥 𝑅
2 nfoi.2 𝑥 𝐴
3 df-oi OrdIso ( 𝑅 , 𝐴 ) = if ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) , ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑎 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑎 ) 𝑧 𝑅 𝑡 } ) , ∅ )
4 1 2 nfwe 𝑥 𝑅 We 𝐴
5 1 2 nfse 𝑥 𝑅 Se 𝐴
6 4 5 nfan 𝑥 ( 𝑅 We 𝐴𝑅 Se 𝐴 )
7 nfcv 𝑥 V
8 nfcv 𝑥 ran
9 nfcv 𝑥 𝑗
10 nfcv 𝑥 𝑤
11 9 1 10 nfbr 𝑥 𝑗 𝑅 𝑤
12 8 11 nfralw 𝑥𝑗 ∈ ran 𝑗 𝑅 𝑤
13 12 2 nfrabw 𝑥 { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 }
14 nfcv 𝑥 𝑢
15 nfcv 𝑥 𝑣
16 14 1 15 nfbr 𝑥 𝑢 𝑅 𝑣
17 16 nfn 𝑥 ¬ 𝑢 𝑅 𝑣
18 13 17 nfralw 𝑥𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣
19 18 13 nfriota 𝑥 ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 )
20 7 19 nfmpt 𝑥 ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) )
21 20 nfrecs 𝑥 recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) )
22 nfcv 𝑥 𝑎
23 21 22 nfima 𝑥 ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑎 )
24 nfcv 𝑥 𝑧
25 nfcv 𝑥 𝑡
26 24 1 25 nfbr 𝑥 𝑧 𝑅 𝑡
27 23 26 nfralw 𝑥𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑎 ) 𝑧 𝑅 𝑡
28 2 27 nfrex 𝑥𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑎 ) 𝑧 𝑅 𝑡
29 nfcv 𝑥 On
30 28 29 nfrabw 𝑥 { 𝑎 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑎 ) 𝑧 𝑅 𝑡 }
31 21 30 nfres 𝑥 ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑎 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑎 ) 𝑧 𝑅 𝑡 } )
32 nfcv 𝑥
33 6 31 32 nfif 𝑥 if ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) , ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑎 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑎 ) 𝑧 𝑅 𝑡 } ) , ∅ )
34 3 33 nfcxfr 𝑥 OrdIso ( 𝑅 , 𝐴 )