onprcf1acwevdlem2

	Ref	Expression
Hypotheses	onprcf1acwevdlem2.1	$⊢ R = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y S z))\}$
	onprcf1acwevdlem2.2	$⊢ S = F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\})$
	onprcf1acwevdlem2.3	$⊢ (φ \land u \in On) \to \exists w \in On F (w) We R_{1} (u)$
Assertion	onprcf1acwevdlem2	$⊢ φ \to R We V$

Proof

Step	Hyp	Ref	Expression
1		onprcf1acwevdlem2.1	$⊢ R = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y S z))\}$
2		onprcf1acwevdlem2.2	$⊢ S = F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\})$
3		onprcf1acwevdlem2.3	$⊢ (φ \land u \in On) \to \exists w \in On F (w) We R_{1} (u)$
4		rankon	$⊢ rank (y) \in On$
5	4	onsuci	$⊢ suc rank (y) \in On$
6	3	ralrimiva	$⊢ φ \to \forall u \in On \exists w \in On F (w) We R_{1} (u)$
7		eqidd	$⊢ u = suc rank (y) \to F (w) = F (w)$
8		fveq2	$⊢ u = suc rank (y) \to R_{1} (u) = R_{1} (suc rank (y))$
9	7 8	weeq12d	$⊢ u = suc rank (y) \to (F (w) We R_{1} (u) \leftrightarrow F (w) We R_{1} (suc rank (y)))$
10	9	rexbidv	$⊢ u = suc rank (y) \to (\exists w \in On F (w) We R_{1} (u) \leftrightarrow \exists w \in On F (w) We R_{1} (suc rank (y)))$
11	10	rspcv	$⊢ suc rank (y) \in On \to (\forall u \in On \exists w \in On F (w) We R_{1} (u) \to \exists w \in On F (w) We R_{1} (suc rank (y)))$
12	5 6 11	mpsyl	$⊢ φ \to \exists w \in On F (w) We R_{1} (suc rank (y))$
13	12	alrimiv	$⊢ φ \to \forall y \exists w \in On F (w) We R_{1} (suc rank (y))$
14		vex	$⊢ v \in V$
15	14	rankr1	$⊢ rank (y) = rank (v) \leftrightarrow (\neg v \in R_{1} (rank (y)) \land v \in R_{1} (suc rank (y)))$
16	15	simprbi	$⊢ rank (y) = rank (v) \to v \in R_{1} (suc rank (y))$
17	16	eqcoms	$⊢ rank (v) = rank (y) \to v \in R_{1} (suc rank (y))$
18	17	rgenw	$⊢ \forall v \in V (rank (v) = rank (y) \to v \in R_{1} (suc rank (y)))$
19		rabss	$⊢ \{v \in V \| rank (v) = rank (y)\} \subseteq R_{1} (suc rank (y)) \leftrightarrow \forall v \in V (rank (v) = rank (y) \to v \in R_{1} (suc rank (y)))$
20	18 19	mpbir	$⊢ \{v \in V \| rank (v) = rank (y)\} \subseteq R_{1} (suc rank (y))$
21		nfcv	$⊢ \underline{Ⅎ} w F$
22		nfrab1	$⊢ \underline{Ⅎ} w \{w \in On \| F (w) We R_{1} (suc rank (y))\}$
23	22	nfint	$⊢ \underline{Ⅎ} w ⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\}$
24	21 23	nffv	$⊢ \underline{Ⅎ} w F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\})$
25	2 24	nfcxfr	$⊢ \underline{Ⅎ} w S$
26		nfcv	$⊢ \underline{Ⅎ} w R_{1} (suc rank (y))$
27	25 26	nfwe	$⊢ Ⅎ w S We R_{1} (suc rank (y))$
28		fveq2	$⊢ w = ⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\} \to F (w) = F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\})$
29	28 2	eqtr4di	$⊢ w = ⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\} \to F (w) = S$
30		eqidd	$⊢ w = ⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\} \to R_{1} (suc rank (y)) = R_{1} (suc rank (y))$
31	29 30	weeq12d	$⊢ w = ⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\} \to (F (w) We R_{1} (suc rank (y)) \leftrightarrow S We R_{1} (suc rank (y)))$
32	27 31	onminsb	$⊢ \exists w \in On F (w) We R_{1} (suc rank (y)) \to S We R_{1} (suc rank (y))$
33		wess	$⊢ \{v \in V \| rank (v) = rank (y)\} \subseteq R_{1} (suc rank (y)) \to (S We R_{1} (suc rank (y)) \to S We \{v \in V \| rank (v) = rank (y)\})$
34	20 32 33	mpsyl	$⊢ \exists w \in On F (w) We R_{1} (suc rank (y)) \to S We \{v \in V \| rank (v) = rank (y)\}$
35	34	alimi	$⊢ \forall y \exists w \in On F (w) We R_{1} (suc rank (y)) \to \forall y S We \{v \in V \| rank (v) = rank (y)\}$
36		ralv	$⊢ \forall y \in V S We \{v \in V \| rank (v) = rank (y)\} \leftrightarrow \forall y S We \{v \in V \| rank (v) = rank (y)\}$
37		eqidd	$⊢ q = rank (y) \to F (w) = F (w)$
38		suceq	$⊢ q = rank (y) \to suc q = suc rank (y)$
39	38	fveq2d	$⊢ q = rank (y) \to R_{1} (suc q) = R_{1} (suc rank (y))$
40	37 39	weeq12d	$⊢ q = rank (y) \to (F (w) We R_{1} (suc q) \leftrightarrow F (w) We R_{1} (suc rank (y)))$
41	40	rabbidv	$⊢ q = rank (y) \to \{w \in On \| F (w) We R_{1} (suc q)\} = \{w \in On \| F (w) We R_{1} (suc rank (y))\}$
42	41	inteqd	$⊢ q = rank (y) \to ⋂ \{w \in On \| F (w) We R_{1} (suc q)\} = ⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\}$
43	42	fveq2d	$⊢ q = rank (y) \to F (⋂ \{w \in On \| F (w) We R_{1} (suc q)\}) = F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\})$
44	43 2	eqtr4di	$⊢ q = rank (y) \to F (⋂ \{w \in On \| F (w) We R_{1} (suc q)\}) = S$
45		eqidd	$⊢ t = y \to F (w) = F (w)$
46		fveq2	$⊢ t = y \to rank (t) = rank (y)$
47	46	suceqd	$⊢ t = y \to suc rank (t) = suc rank (y)$
48	47	fveq2d	$⊢ t = y \to R_{1} (suc rank (t)) = R_{1} (suc rank (y))$
49	45 48	weeq12d	$⊢ t = y \to (F (w) We R_{1} (suc rank (t)) \leftrightarrow F (w) We R_{1} (suc rank (y)))$
50	49	rabbidv	$⊢ t = y \to \{w \in On \| F (w) We R_{1} (suc rank (t))\} = \{w \in On \| F (w) We R_{1} (suc rank (y))\}$
51	50	inteqd	$⊢ t = y \to ⋂ \{w \in On \| F (w) We R_{1} (suc rank (t))\} = ⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\}$
52	51	fveq2d	$⊢ t = y \to F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (t))\}) = F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\})$
53	52 2	eqtr4di	$⊢ t = y \to F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (t))\}) = S$
54	1 44 53	werankwe	$⊢ \forall y \in V S We \{v \in V \| rank (v) = rank (y)\} \to R We V$
55	36 54	sylbir	$⊢ \forall y S We \{v \in V \| rank (v) = rank (y)\} \to R We V$
56	13 35 55	3syl	$⊢ φ \to R We V$

Metamath Proof Explorer

Theorem onprcf1acwevdlem2

Proof