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

Metamath Proof Explorer

Theorem aomclem6

Description: Lemma for dfac11 . Transfinite induction, close over z . (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 aomclem6 ( 𝜑 → ( 𝐻 ‘ 𝐴 ) 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 ssid ⊢ 𝐴 ⊆ 𝐴
11 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → 𝐴 ∈ On )
12 sseq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ⊆ 𝐴 ↔ 𝑑 ⊆ 𝐴 ) )
13 12 anbi2d ⊢ ( 𝑐 = 𝑑 → ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) ) )
14 fveq2 ⊢ ( 𝑐 = 𝑑 → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) )
15 fveq2 ⊢ ( 𝑐 = 𝑑 → ( 𝑅1 ‘ 𝑐 ) = ( 𝑅1 ‘ 𝑑 ) )
16 14 15 weeq12d ⊢ ( 𝑐 = 𝑑 → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) )
17 13 16 imbi12d ⊢ ( 𝑐 = 𝑑 → ( ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ) ↔ ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ) )
18 sseq1 ⊢ ( 𝑐 = 𝐴 → ( 𝑐 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
19 18 anbi2d ⊢ ( 𝑐 = 𝐴 → ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) ) )
20 fveq2 ⊢ ( 𝑐 = 𝐴 → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝐴 ) )
21 fveq2 ⊢ ( 𝑐 = 𝐴 → ( 𝑅1 ‘ 𝑐 ) = ( 𝑅1 ‘ 𝐴 ) )
22 20 21 weeq12d ⊢ ( 𝑐 = 𝐴 → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) ) )
23 19 22 imbi12d ⊢ ( 𝑐 = 𝐴 → ( ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ) ↔ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) ) ) )
24 dmeq ⊢ ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → dom 𝑧 = dom ( 𝐻 ↾ 𝑐 ) )
25 24 adantl ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom 𝑧 = dom ( 𝐻 ↾ 𝑐 ) )
26 simpl1 ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝑐 ∈ On )
27 onss ⊢ ( 𝑐 ∈ On → 𝑐 ⊆ On )
28 7 tfr1 ⊢ 𝐻 Fn On
29 fnssres ⊢ ( ( 𝐻 Fn On ∧ 𝑐 ⊆ On ) → ( 𝐻 ↾ 𝑐 ) Fn 𝑐 )
30 28 29 mpan ⊢ ( 𝑐 ⊆ On → ( 𝐻 ↾ 𝑐 ) Fn 𝑐 )
31 fndm ⊢ ( ( 𝐻 ↾ 𝑐 ) Fn 𝑐 → dom ( 𝐻 ↾ 𝑐 ) = 𝑐 )
32 26 27 30 31 4syl ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom ( 𝐻 ↾ 𝑐 ) = 𝑐 )
33 25 32 eqtrd ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom 𝑧 = 𝑐 )
34 33 26 eqeltrd ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom 𝑧 ∈ On )
35 33 eleq2d ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ( 𝑎 ∈ dom 𝑧 ↔ 𝑎 ∈ 𝑐 ) )
36 35 biimpa ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → 𝑎 ∈ 𝑐 )
37 simpll2 ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) )
38 simpl3l ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝜑 )
39 38 adantr ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → 𝜑 )
40 onelss ⊢ ( dom 𝑧 ∈ On → ( 𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧 ) )
41 34 40 syl ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ( 𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧 ) )
42 41 imp ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → 𝑎 ⊆ dom 𝑧 )
43 simpl3r ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝑐 ⊆ 𝐴 )
44 33 43 eqsstrd ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom 𝑧 ⊆ 𝐴 )
45 44 adantr ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → dom 𝑧 ⊆ 𝐴 )
46 42 45 sstrd ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → 𝑎 ⊆ 𝐴 )
47 sseq1 ⊢ ( 𝑑 = 𝑎 → ( 𝑑 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴 ) )
48 47 anbi2d ⊢ ( 𝑑 = 𝑎 → ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) ) )
49 fveq2 ⊢ ( 𝑑 = 𝑎 → ( 𝐻 ‘ 𝑑 ) = ( 𝐻 ‘ 𝑎 ) )
50 fveq2 ⊢ ( 𝑑 = 𝑎 → ( 𝑅1 ‘ 𝑑 ) = ( 𝑅1 ‘ 𝑎 ) )
51 49 50 weeq12d ⊢ ( 𝑑 = 𝑎 → ( ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ↔ ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) )
52 48 51 imbi12d ⊢ ( 𝑑 = 𝑎 → ( ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ↔ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) ) )
53 52 rspcva ⊢ ( ( 𝑎 ∈ 𝑐 ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ) → ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) )
54 53 imp ⊢ ( ( ( 𝑎 ∈ 𝑐 ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ) ∧ ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) ) → ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
55 36 37 39 46 54 syl22anc ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
56 fveq1 ⊢ ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → ( 𝑧 ‘ 𝑎 ) = ( ( 𝐻 ↾ 𝑐 ) ‘ 𝑎 ) )
57 56 ad2antlr ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( 𝑧 ‘ 𝑎 ) = ( ( 𝐻 ↾ 𝑐 ) ‘ 𝑎 ) )
58 fvres ⊢ ( 𝑎 ∈ 𝑐 → ( ( 𝐻 ↾ 𝑐 ) ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) )
59 36 58 syl ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( ( 𝐻 ↾ 𝑐 ) ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) )
60 57 59 eqtrd ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( 𝑧 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) )
61 weeq1 ⊢ ( ( 𝑧 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) → ( ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ↔ ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) )
62 60 61 syl ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ↔ ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) )
63 55 62 mpbird ⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
64 63 ralrimiva ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
65 38 8 syl ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝐴 ∈ On )
66 38 9 syl ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
67 1 2 3 4 5 6 34 64 65 44 66 aomclem5 ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) )
68 33 fveq2d ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ( 𝑅1 ‘ dom 𝑧 ) = ( 𝑅1 ‘ 𝑐 ) )
69 weeq2 ⊢ ( ( 𝑅1 ‘ dom 𝑧 ) = ( 𝑅1 ‘ 𝑐 ) → ( 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
70 68 69 syl ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ( 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
71 67 70 mpbid ⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) )
72 71 ex ⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
73 72 alrimiv ⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ∀ 𝑧 ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
74 nfv ⊢ Ⅎ 𝑑 ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) )
75 nfv ⊢ Ⅎ 𝑧 𝑑 = ( 𝐻 ↾ 𝑐 )
76 nfsbc1v ⊢ Ⅎ 𝑧 [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 )
77 75 76 nfim ⊢ Ⅎ 𝑧 ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) )
78 eqeq1 ⊢ ( 𝑧 = 𝑑 → ( 𝑧 = ( 𝐻 ↾ 𝑐 ) ↔ 𝑑 = ( 𝐻 ↾ 𝑐 ) ) )
79 sbceq1a ⊢ ( 𝑧 = 𝑑 → ( 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
80 78 79 imbi12d ⊢ ( 𝑧 = 𝑑 → ( ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ↔ ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) )
81 74 77 80 cbvalv1 ⊢ ( ∀ 𝑧 ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ↔ ∀ 𝑑 ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
82 73 81 sylib ⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ∀ 𝑑 ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
83 nfsbc1v ⊢ Ⅎ 𝑑 [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 )
84 fnfun ⊢ ( 𝐻 Fn On → Fun 𝐻 )
85 28 84 ax-mp ⊢ Fun 𝐻
86 vex ⊢ 𝑐 ∈ V
87 resfunexg ⊢ ( ( Fun 𝐻 ∧ 𝑐 ∈ V ) → ( 𝐻 ↾ 𝑐 ) ∈ V )
88 85 86 87 mp2an ⊢ ( 𝐻 ↾ 𝑐 ) ∈ V
89 sbceq1a ⊢ ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → ( [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
90 83 88 89 ceqsal ⊢ ( ∀ 𝑑 ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ↔ [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) )
91 82 90 sylib ⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) )
92 sbccow ⊢ ( [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ [ ( 𝐻 ↾ 𝑐 ) / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) )
93 91 92 sylib ⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → [ ( 𝐻 ↾ 𝑐 ) / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) )
94 nfcsb1v ⊢ Ⅎ 𝑧 ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺
95 nfcv ⊢ Ⅎ 𝑧 ( 𝑅1 ‘ 𝑐 )
96 94 95 nfwe ⊢ Ⅎ 𝑧 ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 )
97 csbeq1a ⊢ ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 )
98 weeq1 ⊢ ( 𝐺 = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 → ( 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
99 97 98 syl ⊢ ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → ( 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
100 96 99 sbciegf ⊢ ( ( 𝐻 ↾ 𝑐 ) ∈ V → ( [ ( 𝐻 ↾ 𝑐 ) / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
101 88 100 ax-mp ⊢ ( [ ( 𝐻 ↾ 𝑐 ) / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) )
102 93 101 sylib ⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) )
103 recsval ⊢ ( 𝑐 ∈ On → ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ‘ 𝑐 ) = ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ↾ 𝑐 ) ) )
104 7 fveq1i ⊢ ( 𝐻 ‘ 𝑐 ) = ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ‘ 𝑐 )
105 fvex ⊢ ( 𝑅1 ‘ dom 𝑧 ) ∈ V
106 105 105 xpex ⊢ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ∈ V
107 106 inex2 ⊢ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) ∈ V
108 6 107 eqeltri ⊢ 𝐺 ∈ V
109 108 csbex ⊢ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 ∈ V
110 eqid ⊢ ( 𝑧 ∈ V ↦ 𝐺 ) = ( 𝑧 ∈ V ↦ 𝐺 )
111 110 fvmpts ⊢ ( ( ( 𝐻 ↾ 𝑐 ) ∈ V ∧ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 ∈ V ) → ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( 𝐻 ↾ 𝑐 ) ) = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 )
112 88 109 111 mp2an ⊢ ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( 𝐻 ↾ 𝑐 ) ) = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺
113 7 reseq1i ⊢ ( 𝐻 ↾ 𝑐 ) = ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ↾ 𝑐 )
114 113 fveq2i ⊢ ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( 𝐻 ↾ 𝑐 ) ) = ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ↾ 𝑐 ) )
115 112 114 eqtr3i ⊢ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 = ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ↾ 𝑐 ) )
116 103 104 115 3eqtr4g ⊢ ( 𝑐 ∈ On → ( 𝐻 ‘ 𝑐 ) = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 )
117 weeq1 ⊢ ( ( 𝐻 ‘ 𝑐 ) = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
118 116 117 syl ⊢ ( 𝑐 ∈ On → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
119 118 3ad2ant1 ⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) )
120 102 119 mpbird ⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) )
121 120 3exp ⊢ ( 𝑐 ∈ On → ( ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) → ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ) ) )
122 17 23 121 tfis3 ⊢ ( 𝐴 ∈ On → ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) ) )
123 11 122 mpcom ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) )
124 10 123 mpan2 ⊢ ( 𝜑 → ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) )