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 ( 𝑅 , 𝐴 )