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 \in V \to F \in V$

Step	Hyp	Ref	Expression
1		oicl.1	$⊢ F = OrdIso (R, A)$
2	1	ordtype	$⊢ (R We A \land R Se A) \to F {Isom}_{E, R} (dom F, A)$
3		isof1o	$⊢ F {Isom}_{E, R} (dom F, A) \to F : dom F \underset{1-1 onto}{⟶} A$
4		f1of1	$⊢ F : dom F \underset{1-1 onto}{⟶} A \to F : dom F \underset{1-1}{⟶} A$
5	2 3 4	3syl	$⊢ (R We A \land R Se A) \to F : dom F \underset{1-1}{⟶} A$
6		f1f	$⊢ F : dom F \underset{1-1}{⟶} A \to F : dom F ⟶ A$
7		f1dmex	$⊢ (F : dom F \underset{1-1}{⟶} A \land A \in V) \to dom F \in V$
8		fex	$⊢ (F : dom F ⟶ A \land dom F \in V) \to F \in V$
9	6 7 8	syl2an2r	$⊢ (F : dom F \underset{1-1}{⟶} A \land A \in V) \to F \in V$
10	9	expcom	$⊢ A \in V \to (F : dom F \underset{1-1}{⟶} A \to F \in V)$
11	5 10	syl5	$⊢ A \in V \to ((R We A \land R Se A) \to F \in V)$
12	1	oi0	$⊢ \neg (R We A \land R Se A) \to F = \emptyset$
13		0ex	$⊢ \emptyset \in V$
14	12 13	eqeltrdi	$⊢ \neg (R We A \land R Se A) \to F \in V$
15	11 14	pm2.61d1	$⊢ A \in V \to F \in V$

Metamath Proof Explorer