aomclem3

Description: Lemma for dfac11 . Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015)

	Ref	Expression
Hypotheses	aomclem3.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)))\}$
	aomclem3.c	$⊢ C = (a \in V ⟼ sup (y (a), R_{1} (dom z), B))$
	aomclem3.d	$⊢ D = recs ((a \in V ⟼ C (R_{1} (dom z) ∖ ran a)))$
	aomclem3.e	$⊢ E = \{⟨a, b⟩ \| ⋂ D^{-1} [\{a\}] \in ⋂ D^{-1} [\{b\}]\}$
	aomclem3.on	$⊢ φ \to dom z \in On$
	aomclem3.su	$⊢ φ \to dom z = suc ⋃ dom z$
	aomclem3.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
	aomclem3.a	$⊢ φ \to A \in On$
	aomclem3.za	$⊢ φ \to dom z \subseteq A$
	aomclem3.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
Assertion	aomclem3	$⊢ φ \to E We R_{1} (dom z)$

Proof

Step	Hyp	Ref	Expression
1		aomclem3.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		aomclem3.c	$⊢ C = (a \in V ⟼ sup (y (a), R_{1} (dom z), B))$
3		aomclem3.d	$⊢ D = recs ((a \in V ⟼ C (R_{1} (dom z) ∖ ran a)))$
4		aomclem3.e	$⊢ E = \{⟨a, b⟩ \| ⋂ D^{-1} [\{a\}] \in ⋂ D^{-1} [\{b\}]\}$
5		aomclem3.on	$⊢ φ \to dom z \in On$
6		aomclem3.su	$⊢ φ \to dom z = suc ⋃ dom z$
7		aomclem3.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
8		aomclem3.a	$⊢ φ \to A \in On$
9		aomclem3.za	$⊢ φ \to dom z \subseteq A$
10		aomclem3.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
11		rneq	$⊢ a = c \to ran a = ran c$
12	11	difeq2d	$⊢ a = c \to R_{1} (dom z) ∖ ran a = R_{1} (dom z) ∖ ran c$
13	12	fveq2d	$⊢ a = c \to C (R_{1} (dom z) ∖ ran a) = C (R_{1} (dom z) ∖ ran c)$
14	13	cbvmptv	$⊢ (a \in V ⟼ C (R_{1} (dom z) ∖ ran a)) = (c \in V ⟼ C (R_{1} (dom z) ∖ ran c))$
15		recseq	$⊢ (a \in V ⟼ C (R_{1} (dom z) ∖ ran a)) = (c \in V ⟼ C (R_{1} (dom z) ∖ ran c)) \to recs ((a \in V ⟼ C (R_{1} (dom z) ∖ ran a))) = recs ((c \in V ⟼ C (R_{1} (dom z) ∖ ran c)))$
16	14 15	ax-mp	$⊢ recs ((a \in V ⟼ C (R_{1} (dom z) ∖ ran a))) = recs ((c \in V ⟼ C (R_{1} (dom z) ∖ ran c)))$
17	3 16	eqtri	$⊢ D = recs ((c \in V ⟼ C (R_{1} (dom z) ∖ ran c)))$
18		fvexd	$⊢ φ \to R_{1} (dom z) \in V$
19	1 2 5 6 7 8 9 10	aomclem2	$⊢ φ \to \forall a \in 𝒫 R_{1} (dom z) (a \neq \emptyset \to C (a) \in a)$
20		neeq1	$⊢ a = d \to (a \neq \emptyset \leftrightarrow d \neq \emptyset)$
21		fveq2	$⊢ a = d \to C (a) = C (d)$
22		id	$⊢ a = d \to a = d$
23	21 22	eleq12d	$⊢ a = d \to (C (a) \in a \leftrightarrow C (d) \in d)$
24	20 23	imbi12d	$⊢ a = d \to ((a \neq \emptyset \to C (a) \in a) \leftrightarrow (d \neq \emptyset \to C (d) \in d))$
25	24	cbvralvw	$⊢ \forall a \in 𝒫 R_{1} (dom z) (a \neq \emptyset \to C (a) \in a) \leftrightarrow \forall d \in 𝒫 R_{1} (dom z) (d \neq \emptyset \to C (d) \in d)$
26	19 25	sylib	$⊢ φ \to \forall d \in 𝒫 R_{1} (dom z) (d \neq \emptyset \to C (d) \in d)$
27	17 18 26 4	dnwech	$⊢ φ \to E We R_{1} (dom z)$

Metamath Proof Explorer

Theorem aomclem3

Proof