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