ordtypelem10

Description: Lemma for ordtype . Using ax-rep , exclude the possibility that O is a proper class and does not enumerate all of A . (Contributed by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Hypotheses	ordtypelem.1	$⊢ F = recs (G)$
	ordtypelem.2	$⊢ C = \{w \in A \| \forall j \in ran h j R w\}$
	ordtypelem.3	$⊢ G = (h \in V ⟼ (ι v \in C \| \forall u \in C \neg u R v))$
	ordtypelem.5	$⊢ T = \{x \in On \| \exists t \in A \forall z \in F [x] z R t\}$
	ordtypelem.6	$⊢ O = OrdIso (R, A)$
	ordtypelem.7	$⊢ φ \to R We A$
	ordtypelem.8	$⊢ φ \to R Se A$
Assertion	ordtypelem10	$⊢ φ \to O {Isom}_{E, R} (dom O, A)$

Proof

Step	Hyp	Ref	Expression
1		ordtypelem.1	$⊢ F = recs (G)$
2		ordtypelem.2	$⊢ C = \{w \in A \| \forall j \in ran h j R w\}$
3		ordtypelem.3	$⊢ G = (h \in V ⟼ (ι v \in C \| \forall u \in C \neg u R v))$
4		ordtypelem.5	$⊢ T = \{x \in On \| \exists t \in A \forall z \in F [x] z R t\}$
5		ordtypelem.6	$⊢ O = OrdIso (R, A)$
6		ordtypelem.7	$⊢ φ \to R We A$
7		ordtypelem.8	$⊢ φ \to R Se A$
8	1 2 3 4 5 6 7	ordtypelem8	$⊢ φ \to O {Isom}_{E, R} (dom O, ran O)$
9	1 2 3 4 5 6 7	ordtypelem4	$⊢ φ \to O : T \cap dom F ⟶ A$
10	9	frnd	$⊢ φ \to ran O \subseteq A$
11		simprl	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to b \in A$
12	6	adantr	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to R We A$
13	7	adantr	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to R Se A$
14	9	ffund	$⊢ φ \to Fun O$
15	14	funfnd	$⊢ φ \to O Fn dom O$
16	15	adantr	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to O Fn dom O$
17	1 2 3 4 5 12 13	ordtypelem8	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to O {Isom}_{E, R} (dom O, ran O)$
18		isof1o	$⊢ O {Isom}_{E, R} (dom O, ran O) \to O : dom O \underset{1-1 onto}{⟶} ran O$
19		f1of1	$⊢ O : dom O \underset{1-1 onto}{⟶} ran O \to O : dom O \underset{1-1}{⟶} ran O$
20	17 18 19	3syl	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to O : dom O \underset{1-1}{⟶} ran O$
21		simpl	$⊢ (b \in A \land \neg b \in ran O) \to b \in A$
22		seex	$⊢ (R Se A \land b \in A) \to \{c \in A \| c R b\} \in V$
23	7 21 22	syl2an	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to \{c \in A \| c R b\} \in V$
24	10	adantr	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to ran O \subseteq A$
25		rexnal	$⊢ \exists m \in dom O \neg O (m) R b \leftrightarrow \neg \forall m \in dom O O (m) R b$
26	1 2 3 4 5 6 7	ordtypelem7	$⊢ ((φ \land b \in A) \land m \in dom O) \to (O (m) R b \lor b \in ran O)$
27	26	ord	$⊢ ((φ \land b \in A) \land m \in dom O) \to (\neg O (m) R b \to b \in ran O)$
28	27	rexlimdva	$⊢ (φ \land b \in A) \to (\exists m \in dom O \neg O (m) R b \to b \in ran O)$
29	25 28	biimtrrid	$⊢ (φ \land b \in A) \to (\neg \forall m \in dom O O (m) R b \to b \in ran O)$
30	29	con1d	$⊢ (φ \land b \in A) \to (\neg b \in ran O \to \forall m \in dom O O (m) R b)$
31	30	impr	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to \forall m \in dom O O (m) R b$
32		breq1	$⊢ c = O (m) \to (c R b \leftrightarrow O (m) R b)$
33	32	ralrn	$⊢ O Fn dom O \to (\forall c \in ran O c R b \leftrightarrow \forall m \in dom O O (m) R b)$
34	16 33	syl	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to (\forall c \in ran O c R b \leftrightarrow \forall m \in dom O O (m) R b)$
35	31 34	mpbird	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to \forall c \in ran O c R b$
36		ssrab	$⊢ ran O \subseteq \{c \in A \| c R b\} \leftrightarrow (ran O \subseteq A \land \forall c \in ran O c R b)$
37	24 35 36	sylanbrc	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to ran O \subseteq \{c \in A \| c R b\}$
38	23 37	ssexd	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to ran O \in V$
39		f1dmex	$⊢ (O : dom O \underset{1-1}{⟶} ran O \land ran O \in V) \to dom O \in V$
40	20 38 39	syl2anc	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to dom O \in V$
41	16 40	fnexd	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to O \in V$
42	1 2 3 4 5 12 13 41	ordtypelem9	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to O {Isom}_{E, R} (dom O, A)$
43		isof1o	$⊢ O {Isom}_{E, R} (dom O, A) \to O : dom O \underset{1-1 onto}{⟶} A$
44		f1ofo	$⊢ O : dom O \underset{1-1 onto}{⟶} A \to O : dom O \underset{onto}{⟶} A$
45		forn	$⊢ O : dom O \underset{onto}{⟶} A \to ran O = A$
46	42 43 44 45	4syl	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to ran O = A$
47	11 46	eleqtrrd	$⊢ (φ \land (b \in A \land \neg b \in ran O)) \to b \in ran O$
48	47	expr	$⊢ (φ \land b \in A) \to (\neg b \in ran O \to b \in ran O)$
49	48	pm2.18d	$⊢ (φ \land b \in A) \to b \in ran O$
50	10 49	eqelssd	$⊢ φ \to ran O = A$
51		isoeq5	$⊢ ran O = A \to (O {Isom}_{E, R} (dom O, ran O) \leftrightarrow O {Isom}_{E, R} (dom O, A))$
52	50 51	syl	$⊢ φ \to (O {Isom}_{E, R} (dom O, ran O) \leftrightarrow O {Isom}_{E, R} (dom O, A))$
53	8 52	mpbid	$⊢ φ \to O {Isom}_{E, R} (dom O, A)$

Metamath Proof Explorer

Theorem ordtypelem10

Proof