ordtypelem7

Description: Lemma for ordtype . ran O is an initial segment of A under the well-order R . (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	ordtypelem7	$⊢ ((φ \land N \in A) \land M \in dom O) \to (O (M) R N \lor N \in ran O)$

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		eldif	$⊢ N \in (A ∖ ran O) \leftrightarrow (N \in A \land \neg N \in ran O)$
9	1 2 3 4 5 6 7	ordtypelem4	$⊢ φ \to O : T \cap dom F ⟶ A$
10	9	adantr	$⊢ (φ \land N \in (A ∖ ran O)) \to O : T \cap dom F ⟶ A$
11	10	fdmd	$⊢ (φ \land N \in (A ∖ ran O)) \to dom O = T \cap dom F$
12		inss1	$⊢ T \cap dom F \subseteq T$
13	1 2 3 4 5 6 7	ordtypelem2	$⊢ φ \to Ord T$
14	13	adantr	$⊢ (φ \land N \in (A ∖ ran O)) \to Ord T$
15		ordsson	$⊢ Ord T \to T \subseteq On$
16	14 15	syl	$⊢ (φ \land N \in (A ∖ ran O)) \to T \subseteq On$
17	12 16	sstrid	$⊢ (φ \land N \in (A ∖ ran O)) \to T \cap dom F \subseteq On$
18	11 17	eqsstrd	$⊢ (φ \land N \in (A ∖ ran O)) \to dom O \subseteq On$
19	18	sseld	$⊢ (φ \land N \in (A ∖ ran O)) \to (M \in dom O \to M \in On)$
20		eleq1	$⊢ a = b \to (a \in dom O \leftrightarrow b \in dom O)$
21		fveq2	$⊢ a = b \to O (a) = O (b)$
22	21	breq1d	$⊢ a = b \to (O (a) R N \leftrightarrow O (b) R N)$
23	20 22	imbi12d	$⊢ a = b \to ((a \in dom O \to O (a) R N) \leftrightarrow (b \in dom O \to O (b) R N))$
24	23	imbi2d	$⊢ a = b \to (((φ \land N \in (A ∖ ran O)) \to (a \in dom O \to O (a) R N)) \leftrightarrow ((φ \land N \in (A ∖ ran O)) \to (b \in dom O \to O (b) R N)))$
25		eleq1	$⊢ a = M \to (a \in dom O \leftrightarrow M \in dom O)$
26		fveq2	$⊢ a = M \to O (a) = O (M)$
27	26	breq1d	$⊢ a = M \to (O (a) R N \leftrightarrow O (M) R N)$
28	25 27	imbi12d	$⊢ a = M \to ((a \in dom O \to O (a) R N) \leftrightarrow (M \in dom O \to O (M) R N))$
29	28	imbi2d	$⊢ a = M \to (((φ \land N \in (A ∖ ran O)) \to (a \in dom O \to O (a) R N)) \leftrightarrow ((φ \land N \in (A ∖ ran O)) \to (M \in dom O \to O (M) R N)))$
30		r19.21v	$⊢ \forall b \in a ((φ \land N \in (A ∖ ran O)) \to (b \in dom O \to O (b) R N)) \leftrightarrow ((φ \land N \in (A ∖ ran O)) \to \forall b \in a (b \in dom O \to O (b) R N))$
31	1	tfr1a	$⊢ (Fun F \land Lim dom F)$
32	31	simpri	$⊢ Lim dom F$
33		limord	$⊢ Lim dom F \to Ord dom F$
34	32 33	ax-mp	$⊢ Ord dom F$
35		ordin	$⊢ (Ord T \land Ord dom F) \to Ord (T \cap dom F)$
36	14 34 35	sylancl	$⊢ (φ \land N \in (A ∖ ran O)) \to Ord (T \cap dom F)$
37		ordeq	$⊢ dom O = T \cap dom F \to (Ord dom O \leftrightarrow Ord (T \cap dom F))$
38	11 37	syl	$⊢ (φ \land N \in (A ∖ ran O)) \to (Ord dom O \leftrightarrow Ord (T \cap dom F))$
39	36 38	mpbird	$⊢ (φ \land N \in (A ∖ ran O)) \to Ord dom O$
40		ordelss	$⊢ (Ord dom O \land a \in dom O) \to a \subseteq dom O$
41	39 40	sylan	$⊢ ((φ \land N \in (A ∖ ran O)) \land a \in dom O) \to a \subseteq dom O$
42	41	sselda	$⊢ (((φ \land N \in (A ∖ ran O)) \land a \in dom O) \land b \in a) \to b \in dom O$
43		pm5.5	$⊢ b \in dom O \to ((b \in dom O \to O (b) R N) \leftrightarrow O (b) R N)$
44	42 43	syl	$⊢ (((φ \land N \in (A ∖ ran O)) \land a \in dom O) \land b \in a) \to ((b \in dom O \to O (b) R N) \leftrightarrow O (b) R N)$
45	44	ralbidva	$⊢ ((φ \land N \in (A ∖ ran O)) \land a \in dom O) \to (\forall b \in a (b \in dom O \to O (b) R N) \leftrightarrow \forall b \in a O (b) R N)$
46		eldifn	$⊢ N \in (A ∖ ran O) \to \neg N \in ran O$
47	46	ad2antlr	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to \neg N \in ran O$
48	9	ad2antrr	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to O : T \cap dom F ⟶ A$
49	48	ffnd	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to O Fn (T \cap dom F)$
50		simprl	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to a \in dom O$
51	48	fdmd	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to dom O = T \cap dom F$
52	50 51	eleqtrd	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to a \in (T \cap dom F)$
53		fnfvelrn	$⊢ (O Fn (T \cap dom F) \land a \in (T \cap dom F)) \to O (a) \in ran O$
54	49 52 53	syl2anc	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to O (a) \in ran O$
55		eleq1	$⊢ O (a) = N \to (O (a) \in ran O \leftrightarrow N \in ran O)$
56	54 55	syl5ibcom	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to (O (a) = N \to N \in ran O)$
57	47 56	mtod	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to \neg O (a) = N$
58		breq1	$⊢ u = N \to (u R O (a) \leftrightarrow N R O (a))$
59	58	notbid	$⊢ u = N \to (\neg u R O (a) \leftrightarrow \neg N R O (a))$
60	1 2 3 4 5 6 7	ordtypelem1	$⊢ φ \to O = {F ↾}_{T}$
61	60	ad2antrr	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to O = {F ↾}_{T}$
62	61	fveq1d	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to O (a) = ({F ↾}_{T}) (a)$
63	52	elin1d	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to a \in T$
64	63	fvresd	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to ({F ↾}_{T}) (a) = F (a)$
65	62 64	eqtrd	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to O (a) = F (a)$
66		simpll	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to φ$
67	1 2 3 4 5 6 7	ordtypelem3	$⊢ (φ \land a \in (T \cap dom F)) \to F (a) \in \{v \in \{w \in A \| \forall j \in F [a] j R w\} \| \forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R v\}$
68	66 52 67	syl2anc	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to F (a) \in \{v \in \{w \in A \| \forall j \in F [a] j R w\} \| \forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R v\}$
69	65 68	eqeltrd	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to O (a) \in \{v \in \{w \in A \| \forall j \in F [a] j R w\} \| \forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R v\}$
70		breq2	$⊢ v = O (a) \to (u R v \leftrightarrow u R O (a))$
71	70	notbid	$⊢ v = O (a) \to (\neg u R v \leftrightarrow \neg u R O (a))$
72	71	ralbidv	$⊢ v = O (a) \to (\forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R v \leftrightarrow \forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R O (a))$
73	72	elrab	$⊢ O (a) \in \{v \in \{w \in A \| \forall j \in F [a] j R w\} \| \forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R v\} \leftrightarrow (O (a) \in \{w \in A \| \forall j \in F [a] j R w\} \land \forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R O (a))$
74	73	simprbi	$⊢ O (a) \in \{v \in \{w \in A \| \forall j \in F [a] j R w\} \| \forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R v\} \to \forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R O (a)$
75	69 74	syl	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to \forall u \in \{w \in A \| \forall j \in F [a] j R w\} \neg u R O (a)$
76		breq2	$⊢ w = N \to (j R w \leftrightarrow j R N)$
77	76	ralbidv	$⊢ w = N \to (\forall j \in F [a] j R w \leftrightarrow \forall j \in F [a] j R N)$
78		eldifi	$⊢ N \in (A ∖ ran O) \to N \in A$
79	78	ad2antlr	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to N \in A$
80		simprr	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to \forall b \in a O (b) R N$
81	41	adantrr	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to a \subseteq dom O$
82	48 81	fssdmd	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to a \subseteq T \cap dom F$
83	82 12	sstrdi	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to a \subseteq T$
84		fveq1	$⊢ O = {F ↾}_{T} \to O (b) = ({F ↾}_{T}) (b)$
85		ssel2	$⊢ (a \subseteq T \land b \in a) \to b \in T$
86	85	fvresd	$⊢ (a \subseteq T \land b \in a) \to ({F ↾}_{T}) (b) = F (b)$
87	84 86	sylan9eq	$⊢ (O = {F ↾}_{T} \land (a \subseteq T \land b \in a)) \to O (b) = F (b)$
88	87	anassrs	$⊢ ((O = {F ↾}_{T} \land a \subseteq T) \land b \in a) \to O (b) = F (b)$
89	88	breq1d	$⊢ ((O = {F ↾}_{T} \land a \subseteq T) \land b \in a) \to (O (b) R N \leftrightarrow F (b) R N)$
90	89	ralbidva	$⊢ (O = {F ↾}_{T} \land a \subseteq T) \to (\forall b \in a O (b) R N \leftrightarrow \forall b \in a F (b) R N)$
91	61 83 90	syl2anc	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to (\forall b \in a O (b) R N \leftrightarrow \forall b \in a F (b) R N)$
92	80 91	mpbid	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to \forall b \in a F (b) R N$
93	31	simpli	$⊢ Fun F$
94		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
95	93 94	mpbi	$⊢ F Fn dom F$
96		inss2	$⊢ T \cap dom F \subseteq dom F$
97	82 96	sstrdi	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to a \subseteq dom F$
98		breq1	$⊢ j = F (b) \to (j R N \leftrightarrow F (b) R N)$
99	98	ralima	$⊢ (F Fn dom F \land a \subseteq dom F) \to (\forall j \in F [a] j R N \leftrightarrow \forall b \in a F (b) R N)$
100	95 97 99	sylancr	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to (\forall j \in F [a] j R N \leftrightarrow \forall b \in a F (b) R N)$
101	92 100	mpbird	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to \forall j \in F [a] j R N$
102	77 79 101	elrabd	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to N \in \{w \in A \| \forall j \in F [a] j R w\}$
103	59 75 102	rspcdva	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to \neg N R O (a)$
104		weso	$⊢ R We A \to R Or A$
105	6 104	syl	$⊢ φ \to R Or A$
106	105	ad2antrr	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to R Or A$
107	48 52	ffvelrnd	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to O (a) \in A$
108		sotric	$⊢ (R Or A \land (O (a) \in A \land N \in A)) \to (O (a) R N \leftrightarrow \neg (O (a) = N \lor N R O (a)))$
109	106 107 79 108	syl12anc	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to (O (a) R N \leftrightarrow \neg (O (a) = N \lor N R O (a)))$
110		ioran	$⊢ \neg (O (a) = N \lor N R O (a)) \leftrightarrow (\neg O (a) = N \land \neg N R O (a))$
111	109 110	bitrdi	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to (O (a) R N \leftrightarrow (\neg O (a) = N \land \neg N R O (a)))$
112	57 103 111	mpbir2and	$⊢ ((φ \land N \in (A ∖ ran O)) \land (a \in dom O \land \forall b \in a O (b) R N)) \to O (a) R N$
113	112	expr	$⊢ ((φ \land N \in (A ∖ ran O)) \land a \in dom O) \to (\forall b \in a O (b) R N \to O (a) R N)$
114	45 113	sylbid	$⊢ ((φ \land N \in (A ∖ ran O)) \land a \in dom O) \to (\forall b \in a (b \in dom O \to O (b) R N) \to O (a) R N)$
115	114	ex	$⊢ (φ \land N \in (A ∖ ran O)) \to (a \in dom O \to (\forall b \in a (b \in dom O \to O (b) R N) \to O (a) R N))$
116	115	com23	$⊢ (φ \land N \in (A ∖ ran O)) \to (\forall b \in a (b \in dom O \to O (b) R N) \to (a \in dom O \to O (a) R N))$
117	116	a2i	$⊢ ((φ \land N \in (A ∖ ran O)) \to \forall b \in a (b \in dom O \to O (b) R N)) \to ((φ \land N \in (A ∖ ran O)) \to (a \in dom O \to O (a) R N))$
118	117	a1i	$⊢ a \in On \to (((φ \land N \in (A ∖ ran O)) \to \forall b \in a (b \in dom O \to O (b) R N)) \to ((φ \land N \in (A ∖ ran O)) \to (a \in dom O \to O (a) R N)))$
119	30 118	syl5bi	$⊢ a \in On \to (\forall b \in a ((φ \land N \in (A ∖ ran O)) \to (b \in dom O \to O (b) R N)) \to ((φ \land N \in (A ∖ ran O)) \to (a \in dom O \to O (a) R N)))$
120	24 29 119	tfis3	$⊢ M \in On \to ((φ \land N \in (A ∖ ran O)) \to (M \in dom O \to O (M) R N))$
121	120	com3l	$⊢ (φ \land N \in (A ∖ ran O)) \to (M \in dom O \to (M \in On \to O (M) R N))$
122	19 121	mpdd	$⊢ (φ \land N \in (A ∖ ran O)) \to (M \in dom O \to O (M) R N)$
123	8 122	sylan2br	$⊢ (φ \land (N \in A \land \neg N \in ran O)) \to (M \in dom O \to O (M) R N)$
124	123	anassrs	$⊢ ((φ \land N \in A) \land \neg N \in ran O) \to (M \in dom O \to O (M) R N)$
125	124	impancom	$⊢ ((φ \land N \in A) \land M \in dom O) \to (\neg N \in ran O \to O (M) R N)$
126	125	orrd	$⊢ ((φ \land N \in A) \land M \in dom O) \to (N \in ran O \lor O (M) R N)$
127	126	orcomd	$⊢ ((φ \land N \in A) \land M \in dom O) \to (O (M) R N \lor N \in ran O)$

Metamath Proof Explorer

Theorem ordtypelem7

Proof