This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )