aomclem5

Description: Lemma for dfac11 . Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Hypotheses	aomclem5.b	$⊢ B = \{⟨a, b⟩ \| \exists c \in R_{1} (⋃ dom z) ((c \in b \land \neg c \in a) \land \forall d \in R_{1} (⋃ dom z) (d z (⋃ dom z) c \to (d \in a \leftrightarrow d \in b)))\}$
	aomclem5.c	$⊢ C = (a \in V ⟼ sup (y (a), R_{1} (dom z), B))$
	aomclem5.d	$⊢ D = recs ((a \in V ⟼ C (R_{1} (dom z) ∖ ran a)))$
	aomclem5.e	$⊢ E = \{⟨a, b⟩ \| ⋂ D^{-1} [\{a\}] \in ⋂ D^{-1} [\{b\}]\}$
	aomclem5.f	$⊢ F = \{⟨a, b⟩ \| (rank (a) E rank (b) \lor (rank (a) = rank (b) \land a z (suc rank (a)) b))\}$
	aomclem5.g	$⊢ G = if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z))$
	aomclem5.on	$⊢ φ \to dom z \in On$
	aomclem5.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
	aomclem5.a	$⊢ φ \to A \in On$
	aomclem5.za	$⊢ φ \to dom z \subseteq A$
	aomclem5.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
Assertion	aomclem5	$⊢ φ \to G We R_{1} (dom z)$

Proof

Step	Hyp	Ref	Expression
1		aomclem5.b	$⊢ B = \{⟨a, b⟩ \| \exists c \in R_{1} (⋃ dom z) ((c \in b \land \neg c \in a) \land \forall d \in R_{1} (⋃ dom z) (d z (⋃ dom z) c \to (d \in a \leftrightarrow d \in b)))\}$
2		aomclem5.c	$⊢ C = (a \in V ⟼ sup (y (a), R_{1} (dom z), B))$
3		aomclem5.d	$⊢ D = recs ((a \in V ⟼ C (R_{1} (dom z) ∖ ran a)))$
4		aomclem5.e	$⊢ E = \{⟨a, b⟩ \| ⋂ D^{-1} [\{a\}] \in ⋂ D^{-1} [\{b\}]\}$
5		aomclem5.f	$⊢ F = \{⟨a, b⟩ \| (rank (a) E rank (b) \lor (rank (a) = rank (b) \land a z (suc rank (a)) b))\}$
6		aomclem5.g	$⊢ G = if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z))$
7		aomclem5.on	$⊢ φ \to dom z \in On$
8		aomclem5.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
9		aomclem5.a	$⊢ φ \to A \in On$
10		aomclem5.za	$⊢ φ \to dom z \subseteq A$
11		aomclem5.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
12	7	adantr	$⊢ (φ \land dom z = ⋃ dom z) \to dom z \in On$
13		simpr	$⊢ (φ \land dom z = ⋃ dom z) \to dom z = ⋃ dom z$
14	8	adantr	$⊢ (φ \land dom z = ⋃ dom z) \to \forall a \in dom z z (a) We R_{1} (a)$
15	5 12 13 14	aomclem4	$⊢ (φ \land dom z = ⋃ dom z) \to F We R_{1} (dom z)$
16		iftrue	$⊢ dom z = ⋃ dom z \to if (dom z = ⋃ dom z, F, E) = F$
17	16	adantl	$⊢ (φ \land dom z = ⋃ dom z) \to if (dom z = ⋃ dom z, F, E) = F$
18		eqidd	$⊢ (φ \land dom z = ⋃ dom z) \to R_{1} (dom z) = R_{1} (dom z)$
19	17 18	weeq12d	$⊢ (φ \land dom z = ⋃ dom z) \to (if (dom z = ⋃ dom z, F, E) We R_{1} (dom z) \leftrightarrow F We R_{1} (dom z))$
20	15 19	mpbird	$⊢ (φ \land dom z = ⋃ dom z) \to if (dom z = ⋃ dom z, F, E) We R_{1} (dom z)$
21	7	adantr	$⊢ (φ \land \neg dom z = ⋃ dom z) \to dom z \in On$
22		eloni	$⊢ dom z \in On \to Ord dom z$
23		orduniorsuc	$⊢ Ord dom z \to (dom z = ⋃ dom z \lor dom z = suc ⋃ dom z)$
24	7 22 23	3syl	$⊢ φ \to (dom z = ⋃ dom z \lor dom z = suc ⋃ dom z)$
25	24	orcanai	$⊢ (φ \land \neg dom z = ⋃ dom z) \to dom z = suc ⋃ dom z$
26	8	adantr	$⊢ (φ \land \neg dom z = ⋃ dom z) \to \forall a \in dom z z (a) We R_{1} (a)$
27	9	adantr	$⊢ (φ \land \neg dom z = ⋃ dom z) \to A \in On$
28	10	adantr	$⊢ (φ \land \neg dom z = ⋃ dom z) \to dom z \subseteq A$
29	11	adantr	$⊢ (φ \land \neg dom z = ⋃ dom z) \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
30	1 2 3 4 21 25 26 27 28 29	aomclem3	$⊢ (φ \land \neg dom z = ⋃ dom z) \to E We R_{1} (dom z)$
31		iffalse	$⊢ \neg dom z = ⋃ dom z \to if (dom z = ⋃ dom z, F, E) = E$
32	31	adantl	$⊢ (φ \land \neg dom z = ⋃ dom z) \to if (dom z = ⋃ dom z, F, E) = E$
33		eqidd	$⊢ (φ \land \neg dom z = ⋃ dom z) \to R_{1} (dom z) = R_{1} (dom z)$
34	32 33	weeq12d	$⊢ (φ \land \neg dom z = ⋃ dom z) \to (if (dom z = ⋃ dom z, F, E) We R_{1} (dom z) \leftrightarrow E We R_{1} (dom z))$
35	30 34	mpbird	$⊢ (φ \land \neg dom z = ⋃ dom z) \to if (dom z = ⋃ dom z, F, E) We R_{1} (dom z)$
36	20 35	pm2.61dan	$⊢ φ \to if (dom z = ⋃ dom z, F, E) We R_{1} (dom z)$
37		weinxp	$⊢ if (dom z = ⋃ dom z, F, E) We R_{1} (dom z) \leftrightarrow (if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z))) We R_{1} (dom z)$
38	36 37	sylib	$⊢ φ \to (if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z))) We R_{1} (dom z)$
39		weeq1	$⊢ G = if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z)) \to (G We R_{1} (dom z) \leftrightarrow (if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z))) We R_{1} (dom z))$
40	6 39	ax-mp	$⊢ G We R_{1} (dom z) \leftrightarrow (if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z))) We R_{1} (dom z)$
41	38 40	sylibr	$⊢ φ \to G We R_{1} (dom z)$

Metamath Proof Explorer

Theorem aomclem5

Proof