ordtypelem9

Description: Lemma for ordtype . Either the function OrdIso is an isomorphism onto all of A , or OrdIso is not a set, which by oif implies that either ran O C_ A is a proper class or dom O = On . (Contributed by Mario Carneiro, 25-Jun-2015) (Revised by AV, 28-Jul-2024)

	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$
	ordtypelem9.1	$⊢ φ \to O \in V$
Assertion	ordtypelem9	$⊢ φ \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		ordtypelem9.1	$⊢ φ \to O \in V$
9	1 2 3 4 5 6 7	ordtypelem8	$⊢ φ \to O {Isom}_{E, R} (dom O, ran O)$
10	1 2 3 4 5 6 7	ordtypelem4	$⊢ φ \to O : T \cap dom F ⟶ A$
11	10	frnd	$⊢ φ \to ran O \subseteq A$
12	1 2 3 4 5 6 7	ordtypelem2	$⊢ φ \to Ord T$
13		ordirr	$⊢ Ord T \to \neg T \in T$
14	12 13	syl	$⊢ φ \to \neg T \in T$
15	1	tfr1a	$⊢ (Fun F \land Lim dom F)$
16	15	simpri	$⊢ Lim dom F$
17		limord	$⊢ Lim dom F \to Ord dom F$
18	16 17	ax-mp	$⊢ Ord dom F$
19	1 2 3 4 5 6 7	ordtypelem1	$⊢ φ \to O = {F ↾}_{T}$
20	8	elexd	$⊢ φ \to O \in V$
21	19 20	eqeltrrd	$⊢ φ \to {F ↾}_{T} \in V$
22	1	tfr2b	$⊢ Ord T \to (T \in dom F \leftrightarrow {F ↾}_{T} \in V)$
23	12 22	syl	$⊢ φ \to (T \in dom F \leftrightarrow {F ↾}_{T} \in V)$
24	21 23	mpbird	$⊢ φ \to T \in dom F$
25		ordelon	$⊢ (Ord dom F \land T \in dom F) \to T \in On$
26	18 24 25	sylancr	$⊢ φ \to T \in On$
27		imaeq2	$⊢ a = T \to F [a] = F [T]$
28	27	raleqdv	$⊢ a = T \to (\forall c \in F [a] c R b \leftrightarrow \forall c \in F [T] c R b)$
29	28	rexbidv	$⊢ a = T \to (\exists b \in A \forall c \in F [a] c R b \leftrightarrow \exists b \in A \forall c \in F [T] c R b)$
30		breq1	$⊢ z = c \to (z R t \leftrightarrow c R t)$
31	30	cbvralvw	$⊢ \forall z \in F [x] z R t \leftrightarrow \forall c \in F [x] c R t$
32		breq2	$⊢ t = b \to (c R t \leftrightarrow c R b)$
33	32	ralbidv	$⊢ t = b \to (\forall c \in F [x] c R t \leftrightarrow \forall c \in F [x] c R b)$
34	31 33	bitrid	$⊢ t = b \to (\forall z \in F [x] z R t \leftrightarrow \forall c \in F [x] c R b)$
35	34	cbvrexvw	$⊢ \exists t \in A \forall z \in F [x] z R t \leftrightarrow \exists b \in A \forall c \in F [x] c R b$
36		imaeq2	$⊢ x = a \to F [x] = F [a]$
37	36	raleqdv	$⊢ x = a \to (\forall c \in F [x] c R b \leftrightarrow \forall c \in F [a] c R b)$
38	37	rexbidv	$⊢ x = a \to (\exists b \in A \forall c \in F [x] c R b \leftrightarrow \exists b \in A \forall c \in F [a] c R b)$
39	35 38	bitrid	$⊢ x = a \to (\exists t \in A \forall z \in F [x] z R t \leftrightarrow \exists b \in A \forall c \in F [a] c R b)$
40	39	cbvrabv	$⊢ \{x \in On \| \exists t \in A \forall z \in F [x] z R t\} = \{a \in On \| \exists b \in A \forall c \in F [a] c R b\}$
41	4 40	eqtri	$⊢ T = \{a \in On \| \exists b \in A \forall c \in F [a] c R b\}$
42	29 41	elrab2	$⊢ T \in T \leftrightarrow (T \in On \land \exists b \in A \forall c \in F [T] c R b)$
43	42	baib	$⊢ T \in On \to (T \in T \leftrightarrow \exists b \in A \forall c \in F [T] c R b)$
44	26 43	syl	$⊢ φ \to (T \in T \leftrightarrow \exists b \in A \forall c \in F [T] c R b)$
45	14 44	mtbid	$⊢ φ \to \neg \exists b \in A \forall c \in F [T] c R b$
46		ralnex	$⊢ \forall b \in A \neg \forall c \in F [T] c R b \leftrightarrow \neg \exists b \in A \forall c \in F [T] c R b$
47	45 46	sylibr	$⊢ φ \to \forall b \in A \neg \forall c \in F [T] c R b$
48	47	r19.21bi	$⊢ (φ \land b \in A) \to \neg \forall c \in F [T] c R b$
49	19	rneqd	$⊢ φ \to ran O = ran ({F ↾}_{T})$
50		df-ima	$⊢ F [T] = ran ({F ↾}_{T})$
51	49 50	eqtr4di	$⊢ φ \to ran O = F [T]$
52	51	adantr	$⊢ (φ \land b \in A) \to ran O = F [T]$
53	52	raleqdv	$⊢ (φ \land b \in A) \to (\forall c \in ran O c R b \leftrightarrow \forall c \in F [T] c R b)$
54	10	ffund	$⊢ φ \to Fun O$
55	54	funfnd	$⊢ φ \to O Fn dom O$
56	55	adantr	$⊢ (φ \land b \in A) \to O Fn dom O$
57		breq1	$⊢ c = O (m) \to (c R b \leftrightarrow O (m) R b)$
58	57	ralrn	$⊢ O Fn dom O \to (\forall c \in ran O c R b \leftrightarrow \forall m \in dom O O (m) R b)$
59	56 58	syl	$⊢ (φ \land b \in A) \to (\forall c \in ran O c R b \leftrightarrow \forall m \in dom O O (m) R b)$
60	53 59	bitr3d	$⊢ (φ \land b \in A) \to (\forall c \in F [T] c R b \leftrightarrow \forall m \in dom O O (m) R b)$
61	48 60	mtbid	$⊢ (φ \land b \in A) \to \neg \forall m \in dom O O (m) R b$
62		rexnal	$⊢ \exists m \in dom O \neg O (m) R b \leftrightarrow \neg \forall m \in dom O O (m) R b$
63	61 62	sylibr	$⊢ (φ \land b \in A) \to \exists m \in dom O \neg O (m) R b$
64	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)$
65	64	ord	$⊢ ((φ \land b \in A) \land m \in dom O) \to (\neg O (m) R b \to b \in ran O)$
66	65	rexlimdva	$⊢ (φ \land b \in A) \to (\exists m \in dom O \neg O (m) R b \to b \in ran O)$
67	63 66	mpd	$⊢ (φ \land b \in A) \to b \in ran O$
68	11 67	eqelssd	$⊢ φ \to ran O = A$
69		isoeq5	$⊢ ran O = A \to (O {Isom}_{E, R} (dom O, ran O) \leftrightarrow O {Isom}_{E, R} (dom O, A))$
70	68 69	syl	$⊢ φ \to (O {Isom}_{E, R} (dom O, ran O) \leftrightarrow O {Isom}_{E, R} (dom O, A))$
71	9 70	mpbid	$⊢ φ \to O {Isom}_{E, R} (dom O, A)$

Metamath Proof Explorer

Theorem ordtypelem9

Proof