aomclem2

Description: Lemma for dfac11 . Successor case 2, a choice function for subsets of ( R1dom z ) . (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypotheses	aomclem2.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)))\}$
	aomclem2.c	$⊢ C = (a \in V ⟼ sup (y (a), R_{1} (dom z), B))$
	aomclem2.on	$⊢ φ \to dom z \in On$
	aomclem2.su	$⊢ φ \to dom z = suc ⋃ dom z$
	aomclem2.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
	aomclem2.a	$⊢ φ \to A \in On$
	aomclem2.za	$⊢ φ \to dom z \subseteq A$
	aomclem2.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
Assertion	aomclem2	$⊢ φ \to \forall a \in 𝒫 R_{1} (dom z) (a \neq \emptyset \to C (a) \in a)$

Proof

Step	Hyp	Ref	Expression
1		aomclem2.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		aomclem2.c	$⊢ C = (a \in V ⟼ sup (y (a), R_{1} (dom z), B))$
3		aomclem2.on	$⊢ φ \to dom z \in On$
4		aomclem2.su	$⊢ φ \to dom z = suc ⋃ dom z$
5		aomclem2.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
6		aomclem2.a	$⊢ φ \to A \in On$
7		aomclem2.za	$⊢ φ \to dom z \subseteq A$
8		aomclem2.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
9		vex	$⊢ a \in V$
10	3 6	jca	$⊢ φ \to (dom z \in On \land A \in On)$
11		r1ord3	$⊢ (dom z \in On \land A \in On) \to (dom z \subseteq A \to R_{1} (dom z) \subseteq R_{1} (A))$
12	10 7 11	sylc	$⊢ φ \to R_{1} (dom z) \subseteq R_{1} (A)$
13	12	sspwd	$⊢ φ \to 𝒫 R_{1} (dom z) \subseteq 𝒫 R_{1} (A)$
14	13	sseld	$⊢ φ \to (a \in 𝒫 R_{1} (dom z) \to a \in 𝒫 R_{1} (A))$
15		rsp	$⊢ \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\})) \to (a \in 𝒫 R_{1} (A) \to (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\})))$
16	8 14 15	sylsyld	$⊢ φ \to (a \in 𝒫 R_{1} (dom z) \to (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\})))$
17	16	3imp	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\})$
18	17	eldifad	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to y (a) \in (𝒫 a \cap Fin)$
19		inss1	$⊢ 𝒫 a \cap Fin \subseteq 𝒫 a$
20	19	sseli	$⊢ y (a) \in (𝒫 a \cap Fin) \to y (a) \in 𝒫 a$
21	20	elpwid	$⊢ y (a) \in (𝒫 a \cap Fin) \to y (a) \subseteq a$
22	18 21	syl	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to y (a) \subseteq a$
23	1 3 4 5	aomclem1	$⊢ φ \to B Or R_{1} (dom z)$
24	23	3ad2ant1	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to B Or R_{1} (dom z)$
25		inss2	$⊢ 𝒫 a \cap Fin \subseteq Fin$
26	25 18	sselid	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to y (a) \in Fin$
27		eldifsni	$⊢ y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}) \to y (a) \neq \emptyset$
28	17 27	syl	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to y (a) \neq \emptyset$
29		elpwi	$⊢ a \in 𝒫 R_{1} (dom z) \to a \subseteq R_{1} (dom z)$
30	29	3ad2ant2	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to a \subseteq R_{1} (dom z)$
31	22 30	sstrd	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to y (a) \subseteq R_{1} (dom z)$
32		fisupcl	$⊢ (B Or R_{1} (dom z) \land (y (a) \in Fin \land y (a) \neq \emptyset \land y (a) \subseteq R_{1} (dom z))) \to sup (y (a), R_{1} (dom z), B) \in y (a)$
33	24 26 28 31 32	syl13anc	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to sup (y (a), R_{1} (dom z), B) \in y (a)$
34	22 33	sseldd	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to sup (y (a), R_{1} (dom z), B) \in a$
35	2	fvmpt2	$⊢ (a \in V \land sup (y (a), R_{1} (dom z), B) \in a) \to C (a) = sup (y (a), R_{1} (dom z), B)$
36	9 34 35	sylancr	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to C (a) = sup (y (a), R_{1} (dom z), B)$
37	36 34	eqeltrd	$⊢ (φ \land a \in 𝒫 R_{1} (dom z) \land a \neq \emptyset) \to C (a) \in a$
38	37	3exp	$⊢ φ \to (a \in 𝒫 R_{1} (dom z) \to (a \neq \emptyset \to C (a) \in a))$
39	38	ralrimiv	$⊢ φ \to \forall a \in 𝒫 R_{1} (dom z) (a \neq \emptyset \to C (a) \in a)$

Metamath Proof Explorer

Theorem aomclem2

Proof