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 ⊢ F = OrdIso R A
Assertion oiexg ⊢ A ∈ V → F ∈ V

Proof

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