aomclem1

Description: Lemma for dfac11 . This is the beginning of the proof that multiple choice is equivalent to choice. Our goal is to construct, by transfinite recursion, a well-ordering of ( R1A ) . In what follows, A is the index of the rank we wish to well-order, z is the collection of well-orderings constructed so far, dom z is the set of ordinal indices of constructed ranks i.e. the next rank to construct, and y is a postulated multiple-choice function.

Successor case 1, define a simple ordering from the well-ordered predecessor. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypotheses	aomclem1.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)))\}$
	aomclem1.on	$⊢ φ \to dom z \in On$
	aomclem1.su	$⊢ φ \to dom z = suc ⋃ dom z$
	aomclem1.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
Assertion	aomclem1	$⊢ φ \to B Or R_{1} (dom z)$

Proof

Step	Hyp	Ref	Expression
1		aomclem1.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		aomclem1.on	$⊢ φ \to dom z \in On$
3		aomclem1.su	$⊢ φ \to dom z = suc ⋃ dom z$
4		aomclem1.we	$⊢ φ \to \forall a \in dom z z (a) We R_{1} (a)$
5		fvex	$⊢ R_{1} (⋃ dom z) \in V$
6		vex	$⊢ z \in V$
7	6	dmex	$⊢ dom z \in V$
8	7	uniex	$⊢ ⋃ dom z \in V$
9	8	sucid	$⊢ ⋃ dom z \in suc ⋃ dom z$
10	9 3	eleqtrrid	$⊢ φ \to ⋃ dom z \in dom z$
11		fveq2	$⊢ a = ⋃ dom z \to z (a) = z (⋃ dom z)$
12		fveq2	$⊢ a = ⋃ dom z \to R_{1} (a) = R_{1} (⋃ dom z)$
13	11 12	weeq12d	$⊢ a = ⋃ dom z \to (z (a) We R_{1} (a) \leftrightarrow z (⋃ dom z) We R_{1} (⋃ dom z))$
14	13	rspcva	$⊢ (⋃ dom z \in dom z \land \forall a \in dom z z (a) We R_{1} (a)) \to z (⋃ dom z) We R_{1} (⋃ dom z)$
15	10 4 14	syl2anc	$⊢ φ \to z (⋃ dom z) We R_{1} (⋃ dom z)$
16	1	wepwso	$⊢ (R_{1} (⋃ dom z) \in V \land z (⋃ dom z) We R_{1} (⋃ dom z)) \to B Or 𝒫 R_{1} (⋃ dom z)$
17	5 15 16	sylancr	$⊢ φ \to B Or 𝒫 R_{1} (⋃ dom z)$
18	3	fveq2d	$⊢ φ \to R_{1} (dom z) = R_{1} (suc ⋃ dom z)$
19		onuni	$⊢ dom z \in On \to ⋃ dom z \in On$
20		r1suc	$⊢ ⋃ dom z \in On \to R_{1} (suc ⋃ dom z) = 𝒫 R_{1} (⋃ dom z)$
21	2 19 20	3syl	$⊢ φ \to R_{1} (suc ⋃ dom z) = 𝒫 R_{1} (⋃ dom z)$
22	18 21	eqtrd	$⊢ φ \to R_{1} (dom z) = 𝒫 R_{1} (⋃ dom z)$
23		soeq2	$⊢ R_{1} (dom z) = 𝒫 R_{1} (⋃ dom z) \to (B Or R_{1} (dom z) \leftrightarrow B Or 𝒫 R_{1} (⋃ dom z))$
24	22 23	syl	$⊢ φ \to (B Or R_{1} (dom z) \leftrightarrow B Or 𝒫 R_{1} (⋃ dom z))$
25	17 24	mpbird	$⊢ φ \to B Or R_{1} (dom z)$

Metamath Proof Explorer

Theorem aomclem1

Proof