aomclem4

Description: Lemma for dfac11 . Limit case. Patch together well-orderings constructed so far using fnwe2 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Hypotheses	aomclem4.f	$⊢ F = \{⟨a, b⟩ \| (rank (a) E rank (b) \lor (rank (a) = rank (b) \land a z (suc rank (a)) b))\}$
	aomclem4.on	$⊢ φ \to dom z \in On$
	aomclem4.su	$⊢ φ \to dom z = ⋃ dom z$
	aomclem4.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
Assertion	aomclem4	$⊢ φ \to F We R_{1} (dom z)$

Proof

Step	Hyp	Ref	Expression
1		aomclem4.f	$⊢ F = \{⟨a, b⟩ \| (rank (a) E rank (b) \lor (rank (a) = rank (b) \land a z (suc rank (a)) b))\}$
2		aomclem4.on	$⊢ φ \to dom z \in On$
3		aomclem4.su	$⊢ φ \to dom z = ⋃ dom z$
4		aomclem4.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
5		suceq	$⊢ c = rank (a) \to suc c = suc rank (a)$
6	5	fveq2d	$⊢ c = rank (a) \to z (suc c) = z (suc rank (a))$
7		r1fnon	$⊢ R_{1} Fn On$
8		fnfun	$⊢ R_{1} Fn On \to Fun R_{1}$
9	7 8	ax-mp	$⊢ Fun R_{1}$
10	7	fndmi	$⊢ dom R_{1} = On$
11	10	eqimss2i	$⊢ On \subseteq dom R_{1}$
12	9 11	pm3.2i	$⊢ (Fun R_{1} \land On \subseteq dom R_{1})$
13		funfvima2	$⊢ (Fun R_{1} \land On \subseteq dom R_{1}) \to (dom z \in On \to R_{1} (dom z) \in R_{1} [On])$
14	12 2 13	mpsyl	$⊢ φ \to R_{1} (dom z) \in R_{1} [On]$
15		elssuni	$⊢ R_{1} (dom z) \in R_{1} [On] \to R_{1} (dom z) \subseteq ⋃ R_{1} [On]$
16	14 15	syl	$⊢ φ \to R_{1} (dom z) \subseteq ⋃ R_{1} [On]$
17	16	sselda	$⊢ (φ \land b \in R_{1} (dom z)) \to b \in ⋃ R_{1} [On]$
18		rankidb	$⊢ b \in ⋃ R_{1} [On] \to b \in R_{1} (suc rank (b))$
19	17 18	syl	$⊢ (φ \land b \in R_{1} (dom z)) \to b \in R_{1} (suc rank (b))$
20		suceq	$⊢ rank (b) = rank (a) \to suc rank (b) = suc rank (a)$
21	20	fveq2d	$⊢ rank (b) = rank (a) \to R_{1} (suc rank (b)) = R_{1} (suc rank (a))$
22	21	eleq2d	$⊢ rank (b) = rank (a) \to (b \in R_{1} (suc rank (b)) \leftrightarrow b \in R_{1} (suc rank (a)))$
23	19 22	syl5ibcom	$⊢ (φ \land b \in R_{1} (dom z)) \to (rank (b) = rank (a) \to b \in R_{1} (suc rank (a)))$
24	23	expimpd	$⊢ φ \to ((b \in R_{1} (dom z) \land rank (b) = rank (a)) \to b \in R_{1} (suc rank (a)))$
25	24	ss2abdv	$⊢ φ \to \{b \| (b \in R_{1} (dom z) \land rank (b) = rank (a))\} \subseteq \{b \| b \in R_{1} (suc rank (a))\}$
26		df-rab	$⊢ \{b \in R_{1} (dom z) \| rank (b) = rank (a)\} = \{b \| (b \in R_{1} (dom z) \land rank (b) = rank (a))\}$
27		abid1	$⊢ R_{1} (suc rank (a)) = \{b \| b \in R_{1} (suc rank (a))\}$
28	25 26 27	3sstr4g	$⊢ φ \to \{b \in R_{1} (dom z) \| rank (b) = rank (a)\} \subseteq R_{1} (suc rank (a))$
29	28	adantr	$⊢ (φ \land a \in R_{1} (dom z)) \to \{b \in R_{1} (dom z) \| rank (b) = rank (a)\} \subseteq R_{1} (suc rank (a))$
30		fveq2	$⊢ b = suc rank (a) \to z (b) = z (suc rank (a))$
31		fveq2	$⊢ b = suc rank (a) \to R_{1} (b) = R_{1} (suc rank (a))$
32	30 31	weeq12d	$⊢ b = suc rank (a) \to (z (b) We R_{1} (b) \leftrightarrow z (suc rank (a)) We R_{1} (suc rank (a)))$
33		fveq2	$⊢ a = b \to z (a) = z (b)$
34		fveq2	$⊢ a = b \to R_{1} (a) = R_{1} (b)$
35	33 34	weeq12d	$⊢ a = b \to (z (a) We R_{1} (a) \leftrightarrow z (b) We R_{1} (b))$
36	35	cbvralvw	$⊢ \forall a \in dom z z (a) We R_{1} (a) \leftrightarrow \forall b \in dom z z (b) We R_{1} (b)$
37	4 36	sylib	$⊢ φ \to \forall b \in dom z z (b) We R_{1} (b)$
38	37	adantr	$⊢ (φ \land a \in R_{1} (dom z)) \to \forall b \in dom z z (b) We R_{1} (b)$
39		rankr1ai	$⊢ a \in R_{1} (dom z) \to rank (a) \in dom z$
40	39	adantl	$⊢ (φ \land a \in R_{1} (dom z)) \to rank (a) \in dom z$
41		eloni	$⊢ dom z \in On \to Ord dom z$
42	2 41	syl	$⊢ φ \to Ord dom z$
43		limsuc2	$⊢ (Ord dom z \land dom z = ⋃ dom z) \to (rank (a) \in dom z \leftrightarrow suc rank (a) \in dom z)$
44	42 3 43	syl2anc	$⊢ φ \to (rank (a) \in dom z \leftrightarrow suc rank (a) \in dom z)$
45	44	adantr	$⊢ (φ \land a \in R_{1} (dom z)) \to (rank (a) \in dom z \leftrightarrow suc rank (a) \in dom z)$
46	40 45	mpbid	$⊢ (φ \land a \in R_{1} (dom z)) \to suc rank (a) \in dom z$
47	32 38 46	rspcdva	$⊢ (φ \land a \in R_{1} (dom z)) \to z (suc rank (a)) We R_{1} (suc rank (a))$
48		wess	$⊢ \{b \in R_{1} (dom z) \| rank (b) = rank (a)\} \subseteq R_{1} (suc rank (a)) \to (z (suc rank (a)) We R_{1} (suc rank (a)) \to z (suc rank (a)) We \{b \in R_{1} (dom z) \| rank (b) = rank (a)\})$
49	29 47 48	sylc	$⊢ (φ \land a \in R_{1} (dom z)) \to z (suc rank (a)) We \{b \in R_{1} (dom z) \| rank (b) = rank (a)\}$
50		rankf	$⊢ rank : ⋃ R_{1} [On] ⟶ On$
51	50	a1i	$⊢ φ \to rank : ⋃ R_{1} [On] ⟶ On$
52	51 16	fssresd	$⊢ φ \to ({rank ↾}_{R_{1} (dom z)}) : R_{1} (dom z) ⟶ On$
53		epweon	$⊢ E We On$
54	53	a1i	$⊢ φ \to E We On$
55	6 1 49 52 54	fnwe2	$⊢ φ \to F We R_{1} (dom z)$

Metamath Proof Explorer

Theorem aomclem4

Proof