This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) )