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 
|- F/_ x R
nfoi.2 
|- F/_ x A
Assertion nfoi 
|- F/_ x OrdIso ( R , A )

Proof

Step Hyp Ref Expression
1 nfoi.1 
 |-  F/_ x R
2 nfoi.2 
 |-  F/_ x A
3 df-oi 
 |-  OrdIso ( R , A ) = if ( ( R We A /\ R Se A ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) |` { a e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " a ) z R t } ) , (/) )
4 1 2 nfwe 
 |-  F/ x R We A
5 1 2 nfse 
 |-  F/ x R Se A
6 4 5 nfan 
 |-  F/ x ( R We A /\ R Se A )
7 nfcv 
 |-  F/_ x _V
8 nfcv 
 |-  F/_ x ran h
9 nfcv 
 |-  F/_ x j
10 nfcv 
 |-  F/_ x w
11 9 1 10 nfbr 
 |-  F/ x j R w
12 8 11 nfralw 
 |-  F/ x A. j e. ran h j R w
13 12 2 nfrabw 
 |-  F/_ x { w e. A | A. j e. ran h j R w }
14 nfcv 
 |-  F/_ x u
15 nfcv 
 |-  F/_ x v
16 14 1 15 nfbr 
 |-  F/ x u R v
17 16 nfn 
 |-  F/ x -. u R v
18 13 17 nfralw 
 |-  F/ x A. u e. { w e. A | A. j e. ran h j R w } -. u R v
19 18 13 nfriota 
 |-  F/_ x ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v )
20 7 19 nfmpt 
 |-  F/_ x ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) )
21 20 nfrecs 
 |-  F/_ x recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) )
22 nfcv 
 |-  F/_ x a
23 21 22 nfima 
 |-  F/_ x ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " a )
24 nfcv 
 |-  F/_ x z
25 nfcv 
 |-  F/_ x t
26 24 1 25 nfbr 
 |-  F/ x z R t
27 23 26 nfralw 
 |-  F/ x A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " a ) z R t
28 2 27 nfrex 
 |-  F/ x E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " a ) z R t
29 nfcv 
 |-  F/_ x On
30 28 29 nfrabw 
 |-  F/_ x { a e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " a ) z R t }
31 21 30 nfres 
 |-  F/_ x ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) |` { a e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " a ) z R t } )
32 nfcv 
 |-  F/_ x (/)
33 6 31 32 nfif 
 |-  F/_ x if ( ( R We A /\ R Se A ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) |` { a e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " a ) z R t } ) , (/) )
34 3 33 nfcxfr 
 |-  F/_ x OrdIso ( R , A )