Theorem aomclem7

Description: Lemma for dfac11 . ( R1A ) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Hypotheses	aomclem6.b	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
	aomclem6.c	⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
	aomclem6.d	⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) )
	aomclem6.e	⊢ 𝐸 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) }
	aomclem6.f	⊢ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) }
	aomclem6.g	⊢ 𝐺 = ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) )
	aomclem6.h	⊢ 𝐻 = recs ( ( 𝑧 ∈ V ↦ 𝐺 ) )
	aomclem6.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	aomclem6.y	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
Assertion	aomclem7	⊢ ( 𝜑 → ∃ 𝑏 𝑏 We ( 𝑅1 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		aomclem6.b	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
2		aomclem6.c	⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
3		aomclem6.d	⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) )
4		aomclem6.e	⊢ 𝐸 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) }
5		aomclem6.f	⊢ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) }
6		aomclem6.g	⊢ 𝐺 = ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) )
7		aomclem6.h	⊢ 𝐻 = recs ( ( 𝑧 ∈ V ↦ 𝐺 ) )
8		aomclem6.a	⊢ ( 𝜑 → 𝐴 ∈ On )
9		aomclem6.y	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
10	1 2 3 4 5 6 7 8 9	aomclem6	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) )
11		fvex	⊢ ( 𝐻 ‘ 𝐴 ) ∈ V
12		weeq1	⊢ ( 𝑏 = ( 𝐻 ‘ 𝐴 ) → ( 𝑏 We ( 𝑅1 ‘ 𝐴 ) ↔ ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) ) )
13	11 12	spcev	⊢ ( ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) → ∃ 𝑏 𝑏 We ( 𝑅1 ‘ 𝐴 ) )
14	10 13	syl	⊢ ( 𝜑 → ∃ 𝑏 𝑏 We ( 𝑅1 ‘ 𝐴 ) )