Theorem 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	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
	aomclem1.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
	aomclem1.su	⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
	aomclem1.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
Assertion	aomclem1	⊢ ( 𝜑 → 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		aomclem1.b	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
2		aomclem1.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
3		aomclem1.su	⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
4		aomclem1.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
5		fvex	⊢ ( 𝑅1 ‘ ∪ dom 𝑧 ) ∈ V
6		vex	⊢ 𝑧 ∈ V
7	6	dmex	⊢ dom 𝑧 ∈ V
8	7	uniex	⊢ ∪ dom 𝑧 ∈ V
9	8	sucid	⊢ ∪ dom 𝑧 ∈ suc ∪ dom 𝑧
10	9 3	eleqtrrid	⊢ ( 𝜑 → ∪ dom 𝑧 ∈ dom 𝑧 )
11		fveq2	⊢ ( 𝑎 = ∪ dom 𝑧 → ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ ∪ dom 𝑧 ) )
12		fveq2	⊢ ( 𝑎 = ∪ dom 𝑧 → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ ∪ dom 𝑧 ) )
13	11 12	weeq12d	⊢ ( 𝑎 = ∪ dom 𝑧 → ( ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ↔ ( 𝑧 ‘ ∪ dom 𝑧 ) We ( 𝑅1 ‘ ∪ dom 𝑧 ) ) )
14	13	rspcva	⊢ ( ( ∪ dom 𝑧 ∈ dom 𝑧 ∧ ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) → ( 𝑧 ‘ ∪ dom 𝑧 ) We ( 𝑅1 ‘ ∪ dom 𝑧 ) )
15	10 4 14	syl2anc	⊢ ( 𝜑 → ( 𝑧 ‘ ∪ dom 𝑧 ) We ( 𝑅1 ‘ ∪ dom 𝑧 ) )
16	1	wepwso	⊢ ( ( ( 𝑅1 ‘ ∪ dom 𝑧 ) ∈ V ∧ ( 𝑧 ‘ ∪ dom 𝑧 ) We ( 𝑅1 ‘ ∪ dom 𝑧 ) ) → 𝐵 Or 𝒫 ( 𝑅1 ‘ ∪ dom 𝑧 ) )
17	5 15 16	sylancr	⊢ ( 𝜑 → 𝐵 Or 𝒫 ( 𝑅1 ‘ ∪ dom 𝑧 ) )
18	3	fveq2d	⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) = ( 𝑅1 ‘ suc ∪ dom 𝑧 ) )
19		onuni	⊢ ( dom 𝑧 ∈ On → ∪ dom 𝑧 ∈ On )
20		r1suc	⊢ ( ∪ dom 𝑧 ∈ On → ( 𝑅1 ‘ suc ∪ dom 𝑧 ) = 𝒫 ( 𝑅1 ‘ ∪ dom 𝑧 ) )
21	2 19 20	3syl	⊢ ( 𝜑 → ( 𝑅1 ‘ suc ∪ dom 𝑧 ) = 𝒫 ( 𝑅1 ‘ ∪ dom 𝑧 ) )
22	18 21	eqtrd	⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) = 𝒫 ( 𝑅1 ‘ ∪ dom 𝑧 ) )
23		soeq2	⊢ ( ( 𝑅1 ‘ dom 𝑧 ) = 𝒫 ( 𝑅1 ‘ ∪ dom 𝑧 ) → ( 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐵 Or 𝒫 ( 𝑅1 ‘ ∪ dom 𝑧 ) ) )
24	22 23	syl	⊢ ( 𝜑 → ( 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐵 Or 𝒫 ( 𝑅1 ‘ ∪ dom 𝑧 ) ) )
25	17 24	mpbird	⊢ ( 𝜑 → 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) )