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

Metamath Proof Explorer

Theorem aomclem3

Description: Lemma for dfac11 . Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses aomclem3.b ⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
aomclem3.c ⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
aomclem3.d ⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) )
aomclem3.e ⊢ 𝐸 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) }
aomclem3.on ⊢ ( 𝜑 → dom 𝑧 ∈ On )
aomclem3.su ⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
aomclem3.we ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
aomclem3.a ⊢ ( 𝜑 → 𝐴 ∈ On )
aomclem3.za ⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
aomclem3.y ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
Assertion aomclem3 ( 𝜑 → 𝐸 We ( 𝑅1 ‘ dom 𝑧 ) )

Proof

Step Hyp Ref Expression
1 aomclem3.b ⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
2 aomclem3.c ⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
3 aomclem3.d ⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) )
4 aomclem3.e ⊢ 𝐸 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) }
5 aomclem3.on ⊢ ( 𝜑 → dom 𝑧 ∈ On )
6 aomclem3.su ⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
7 aomclem3.we ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
8 aomclem3.a ⊢ ( 𝜑 → 𝐴 ∈ On )
9 aomclem3.za ⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
10 aomclem3.y ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
11 rneq ⊢ ( 𝑎 = 𝑐 → ran 𝑎 = ran 𝑐 )
12 11 difeq2d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) = ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) )
13 12 fveq2d ⊢ ( 𝑎 = 𝑐 → ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) = ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) )
14 13 cbvmptv ⊢ ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) = ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) )
15 recseq ⊢ ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) = ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) ) → recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) ) = recs ( ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) ) ) )
16 14 15 ax-mp ⊢ recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) ) = recs ( ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) ) )
17 3 16 eqtri ⊢ 𝐷 = recs ( ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) ) )
18 fvexd ⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) ∈ V )
19 1 2 5 6 7 8 9 10 aomclem2 ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) )
20 neeq1 ⊢ ( 𝑎 = 𝑑 → ( 𝑎 ≠ ∅ ↔ 𝑑 ≠ ∅ ) )
21 fveq2 ⊢ ( 𝑎 = 𝑑 → ( 𝐶 ‘ 𝑎 ) = ( 𝐶 ‘ 𝑑 ) )
22 id ⊢ ( 𝑎 = 𝑑 → 𝑎 = 𝑑 )
23 21 22 eleq12d ⊢ ( 𝑎 = 𝑑 → ( ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ↔ ( 𝐶 ‘ 𝑑 ) ∈ 𝑑 ) )
24 20 23 imbi12d ⊢ ( 𝑎 = 𝑑 → ( ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) ↔ ( 𝑑 ≠ ∅ → ( 𝐶 ‘ 𝑑 ) ∈ 𝑑 ) ) )
25 24 cbvralvw ⊢ ( ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) ↔ ∀ 𝑑 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑑 ≠ ∅ → ( 𝐶 ‘ 𝑑 ) ∈ 𝑑 ) )
26 19 25 sylib ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑑 ≠ ∅ → ( 𝐶 ‘ 𝑑 ) ∈ 𝑑 ) )
27 17 18 26 4 dnwech ⊢ ( 𝜑 → 𝐸 We ( 𝑅1 ‘ dom 𝑧 ) )