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

Metamath Proof Explorer

Theorem aomclem5

Description: Lemma for dfac11 . Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 aomclem5.b ⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
2 aomclem5.c ⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
3 aomclem5.d ⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) )
4 aomclem5.e ⊢ 𝐸 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) }
5 aomclem5.f ⊢ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) }
6 aomclem5.g ⊢ 𝐺 = ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) )
7 aomclem5.on ⊢ ( 𝜑 → dom 𝑧 ∈ On )
8 aomclem5.we ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
9 aomclem5.a ⊢ ( 𝜑 → 𝐴 ∈ On )
10 aomclem5.za ⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
11 aomclem5.y ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
12 7 adantr ⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 ∈ On )
13 simpr ⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 = ∪ dom 𝑧 )
14 8 adantr ⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
15 5 12 13 14 aomclem4 ⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → 𝐹 We ( 𝑅1 ‘ dom 𝑧 ) )
16 iftrue ⊢ ( dom 𝑧 = ∪ dom 𝑧 → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) = 𝐹 )
17 16 adantl ⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) = 𝐹 )
18 eqidd ⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → ( 𝑅1 ‘ dom 𝑧 ) = ( 𝑅1 ‘ dom 𝑧 ) )
19 17 18 weeq12d ⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐹 We ( 𝑅1 ‘ dom 𝑧 ) ) )
20 15 19 mpbird ⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) )
21 7 adantr ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 ∈ On )
22 eloni ⊢ ( dom 𝑧 ∈ On → Ord dom 𝑧 )
23 orduniorsuc ⊢ ( Ord dom 𝑧 → ( dom 𝑧 = ∪ dom 𝑧 ∨ dom 𝑧 = suc ∪ dom 𝑧 ) )
24 7 22 23 3syl ⊢ ( 𝜑 → ( dom 𝑧 = ∪ dom 𝑧 ∨ dom 𝑧 = suc ∪ dom 𝑧 ) )
25 24 orcanai ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 = suc ∪ dom 𝑧 )
26 8 adantr ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
27 9 adantr ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → 𝐴 ∈ On )
28 10 adantr ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 ⊆ 𝐴 )
29 11 adantr ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
30 1 2 3 4 21 25 26 27 28 29 aomclem3 ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → 𝐸 We ( 𝑅1 ‘ dom 𝑧 ) )
31 iffalse ⊢ ( ¬ dom 𝑧 = ∪ dom 𝑧 → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) = 𝐸 )
32 31 adantl ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) = 𝐸 )
33 eqidd ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → ( 𝑅1 ‘ dom 𝑧 ) = ( 𝑅1 ‘ dom 𝑧 ) )
34 32 33 weeq12d ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐸 We ( 𝑅1 ‘ dom 𝑧 ) ) )
35 30 34 mpbird ⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) )
36 20 35 pm2.61dan ⊢ ( 𝜑 → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) )
37 weinxp ⊢ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) ↔ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) We ( 𝑅1 ‘ dom 𝑧 ) )
38 36 37 sylib ⊢ ( 𝜑 → ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) We ( 𝑅1 ‘ dom 𝑧 ) )
39 weeq1 ⊢ ( 𝐺 = ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) → ( 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) ↔ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) We ( 𝑅1 ‘ dom 𝑧 ) ) )
40 6 39 ax-mp ⊢ ( 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) ↔ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) We ( 𝑅1 ‘ dom 𝑧 ) )
41 38 40 sylibr ⊢ ( 𝜑 → 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) )