Theorem oiexg

Description: The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Hypothesis	oicl.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
Assertion	oiexg	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		oicl.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
2	1	ordtype	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
3		isof1o	⊢ ( 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) → 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 )
4		f1of1	⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 → 𝐹 : dom 𝐹 –1-1→ 𝐴 )
5	2 3 4	3syl	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 : dom 𝐹 –1-1→ 𝐴 )
6		f1f	⊢ ( 𝐹 : dom 𝐹 –1-1→ 𝐴 → 𝐹 : dom 𝐹 ⟶ 𝐴 )
7		f1dmex	⊢ ( ( 𝐹 : dom 𝐹 –1-1→ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → dom 𝐹 ∈ V )
8		fex	⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ∈ V ) → 𝐹 ∈ V )
9	6 7 8	syl2an2r	⊢ ( ( 𝐹 : dom 𝐹 –1-1→ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
10	9	expcom	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : dom 𝐹 –1-1→ 𝐴 → 𝐹 ∈ V ) )
11	5 10	syl5	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 ∈ V ) )
12	1	oi0	⊢ ( ¬ ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 = ∅ )
13		0ex	⊢ ∅ ∈ V
14	12 13	eqeltrdi	⊢ ( ¬ ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 ∈ V )
15	11 14	pm2.61d1	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 ∈ V )