Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aomclem6 Structured version   Visualization version   GIF version

Theorem aomclem6 41372
Description: Lemma for dfac11 41375. Transfinite induction, close over 𝑧. (Contributed by Stefan O'Rear, 20-Jan-2015.)
Hypotheses
Ref Expression
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
Ref Expression
aomclem6 (𝜑 → (𝐻𝐴) We (𝑅1𝐴))
Distinct variable groups:   𝑦,𝑧,𝑎,𝑏,𝑐,𝑑   𝜑,𝑎,𝑏,𝑐,𝑑,𝑧   𝐶,𝑎,𝑏,𝑐,𝑑   𝐷,𝑎,𝑏,𝑐,𝑑   𝐴,𝑎,𝑏,𝑐,𝑑,𝑧   𝐻,𝑎,𝑏,𝑐,𝑑,𝑧   𝐺,𝑑
Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)   𝐵(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝐶(𝑦,𝑧)   𝐷(𝑦,𝑧)   𝐸(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝐹(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝐺(𝑦,𝑧,𝑎,𝑏,𝑐)   𝐻(𝑦)

Proof of Theorem aomclem6
StepHypRef Expression
1 ssid 3966 . 2 𝐴𝐴
2 aomclem6.a . . . 4 (𝜑𝐴 ∈ On)
32adantr 481 . . 3 ((𝜑𝐴𝐴) → 𝐴 ∈ On)
4 sseq1 3969 . . . . . 6 (𝑐 = 𝑑 → (𝑐𝐴𝑑𝐴))
54anbi2d 629 . . . . 5 (𝑐 = 𝑑 → ((𝜑𝑐𝐴) ↔ (𝜑𝑑𝐴)))
6 fveq2 6842 . . . . . 6 (𝑐 = 𝑑 → (𝐻𝑐) = (𝐻𝑑))
7 fveq2 6842 . . . . . 6 (𝑐 = 𝑑 → (𝑅1𝑐) = (𝑅1𝑑))
86, 7weeq12d 41353 . . . . 5 (𝑐 = 𝑑 → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑑) We (𝑅1𝑑)))
95, 8imbi12d 344 . . . 4 (𝑐 = 𝑑 → (((𝜑𝑐𝐴) → (𝐻𝑐) We (𝑅1𝑐)) ↔ ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑))))
10 sseq1 3969 . . . . . 6 (𝑐 = 𝐴 → (𝑐𝐴𝐴𝐴))
1110anbi2d 629 . . . . 5 (𝑐 = 𝐴 → ((𝜑𝑐𝐴) ↔ (𝜑𝐴𝐴)))
12 fveq2 6842 . . . . . 6 (𝑐 = 𝐴 → (𝐻𝑐) = (𝐻𝐴))
13 fveq2 6842 . . . . . 6 (𝑐 = 𝐴 → (𝑅1𝑐) = (𝑅1𝐴))
1412, 13weeq12d 41353 . . . . 5 (𝑐 = 𝐴 → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝐴) We (𝑅1𝐴)))
1511, 14imbi12d 344 . . . 4 (𝑐 = 𝐴 → (((𝜑𝑐𝐴) → (𝐻𝑐) We (𝑅1𝑐)) ↔ ((𝜑𝐴𝐴) → (𝐻𝐴) We (𝑅1𝐴))))
16 aomclem6.b . . . . . . . . . . . . . 14 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1 dom 𝑧)((𝑐𝑏 ∧ ¬ 𝑐𝑎) ∧ ∀𝑑 ∈ (𝑅1 dom 𝑧)(𝑑(𝑧 dom 𝑧)𝑐 → (𝑑𝑎𝑑𝑏)))}
17 aomclem6.c . . . . . . . . . . . . . 14 𝐶 = (𝑎 ∈ V ↦ sup((𝑦𝑎), (𝑅1‘dom 𝑧), 𝐵))
18 aomclem6.d . . . . . . . . . . . . . 14 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))
19 aomclem6.e . . . . . . . . . . . . . 14 𝐸 = {⟨𝑎, 𝑏⟩ ∣ (𝐷 “ {𝑎}) ∈ (𝐷 “ {𝑏})}
20 aomclem6.f . . . . . . . . . . . . . 14 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}
21 aomclem6.g . . . . . . . . . . . . . 14 𝐺 = (if(dom 𝑧 = dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))
22 dmeq 5859 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝐻𝑐) → dom 𝑧 = dom (𝐻𝑐))
2322adantl 482 . . . . . . . . . . . . . . . 16 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧 = dom (𝐻𝑐))
24 simpl1 1191 . . . . . . . . . . . . . . . . 17 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝑐 ∈ On)
25 onss 7719 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ On → 𝑐 ⊆ On)
26 aomclem6.h . . . . . . . . . . . . . . . . . . 19 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))
2726tfr1 8343 . . . . . . . . . . . . . . . . . 18 𝐻 Fn On
28 fnssres 6624 . . . . . . . . . . . . . . . . . 18 ((𝐻 Fn On ∧ 𝑐 ⊆ On) → (𝐻𝑐) Fn 𝑐)
2927, 28mpan 688 . . . . . . . . . . . . . . . . 17 (𝑐 ⊆ On → (𝐻𝑐) Fn 𝑐)
30 fndm 6605 . . . . . . . . . . . . . . . . 17 ((𝐻𝑐) Fn 𝑐 → dom (𝐻𝑐) = 𝑐)
3124, 25, 29, 304syl 19 . . . . . . . . . . . . . . . 16 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom (𝐻𝑐) = 𝑐)
3223, 31eqtrd 2776 . . . . . . . . . . . . . . 15 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧 = 𝑐)
3332, 24eqeltrd 2838 . . . . . . . . . . . . . 14 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧 ∈ On)
3432eleq2d 2823 . . . . . . . . . . . . . . . . . 18 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝑎 ∈ dom 𝑧𝑎𝑐))
3534biimpa 477 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎𝑐)
36 simpll2 1213 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)))
37 simpl3l 1228 . . . . . . . . . . . . . . . . . 18 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝜑)
3837adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝜑)
39 onelss 6359 . . . . . . . . . . . . . . . . . . . 20 (dom 𝑧 ∈ On → (𝑎 ∈ dom 𝑧𝑎 ⊆ dom 𝑧))
4033, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝑎 ∈ dom 𝑧𝑎 ⊆ dom 𝑧))
4140imp 407 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ dom 𝑧)
42 simpl3r 1229 . . . . . . . . . . . . . . . . . . . 20 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝑐𝐴)
4332, 42eqsstrd 3982 . . . . . . . . . . . . . . . . . . 19 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧𝐴)
4443adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → dom 𝑧𝐴)
4541, 44sstrd 3954 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎𝐴)
46 sseq1 3969 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (𝑑𝐴𝑎𝐴))
4746anbi2d 629 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → ((𝜑𝑑𝐴) ↔ (𝜑𝑎𝐴)))
48 fveq2 6842 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (𝐻𝑑) = (𝐻𝑎))
49 fveq2 6842 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (𝑅1𝑑) = (𝑅1𝑎))
5048, 49weeq12d 41353 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → ((𝐻𝑑) We (𝑅1𝑑) ↔ (𝐻𝑎) We (𝑅1𝑎)))
5147, 50imbi12d 344 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑎 → (((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ↔ ((𝜑𝑎𝐴) → (𝐻𝑎) We (𝑅1𝑎))))
5251rspcva 3579 . . . . . . . . . . . . . . . . . 18 ((𝑎𝑐 ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑))) → ((𝜑𝑎𝐴) → (𝐻𝑎) We (𝑅1𝑎)))
5352imp 407 . . . . . . . . . . . . . . . . 17 (((𝑎𝑐 ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑))) ∧ (𝜑𝑎𝐴)) → (𝐻𝑎) We (𝑅1𝑎))
5435, 36, 38, 45, 53syl22anc 837 . . . . . . . . . . . . . . . 16 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝐻𝑎) We (𝑅1𝑎))
55 fveq1 6841 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐻𝑐) → (𝑧𝑎) = ((𝐻𝑐)‘𝑎))
5655ad2antlr 725 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧𝑎) = ((𝐻𝑐)‘𝑎))
57 fvres 6861 . . . . . . . . . . . . . . . . . . 19 (𝑎𝑐 → ((𝐻𝑐)‘𝑎) = (𝐻𝑎))
5835, 57syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝐻𝑐)‘𝑎) = (𝐻𝑎))
5956, 58eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧𝑎) = (𝐻𝑎))
60 weeq1 5621 . . . . . . . . . . . . . . . . 17 ((𝑧𝑎) = (𝐻𝑎) → ((𝑧𝑎) We (𝑅1𝑎) ↔ (𝐻𝑎) We (𝑅1𝑎)))
6159, 60syl 17 . . . . . . . . . . . . . . . 16 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝑧𝑎) We (𝑅1𝑎) ↔ (𝐻𝑎) We (𝑅1𝑎)))
6254, 61mpbird 256 . . . . . . . . . . . . . . 15 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧𝑎) We (𝑅1𝑎))
6362ralrimiva 3143 . . . . . . . . . . . . . 14 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → ∀𝑎 ∈ dom 𝑧(𝑧𝑎) We (𝑅1𝑎))
6437, 2syl 17 . . . . . . . . . . . . . 14 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝐴 ∈ On)
65 aomclem6.y . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1𝐴)(𝑎 ≠ ∅ → (𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))
6637, 65syl 17 . . . . . . . . . . . . . 14 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → ∀𝑎 ∈ 𝒫 (𝑅1𝐴)(𝑎 ≠ ∅ → (𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))
6716, 17, 18, 19, 20, 21, 33, 63, 64, 43, 66aomclem5 41371 . . . . . . . . . . . . 13 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝐺 We (𝑅1‘dom 𝑧))
6832fveq2d 6846 . . . . . . . . . . . . . 14 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝑅1‘dom 𝑧) = (𝑅1𝑐))
69 weeq2 5622 . . . . . . . . . . . . . 14 ((𝑅1‘dom 𝑧) = (𝑅1𝑐) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1𝑐)))
7068, 69syl 17 . . . . . . . . . . . . 13 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1𝑐)))
7167, 70mpbid 231 . . . . . . . . . . . 12 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝐺 We (𝑅1𝑐))
7271ex 413 . . . . . . . . . . 11 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → (𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)))
7372alrimiv 1930 . . . . . . . . . 10 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → ∀𝑧(𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)))
74 nfv 1917 . . . . . . . . . . 11 𝑑(𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐))
75 nfv 1917 . . . . . . . . . . . 12 𝑧 𝑑 = (𝐻𝑐)
76 nfsbc1v 3759 . . . . . . . . . . . 12 𝑧[𝑑 / 𝑧]𝐺 We (𝑅1𝑐)
7775, 76nfim 1899 . . . . . . . . . . 11 𝑧(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐))
78 eqeq1 2740 . . . . . . . . . . . 12 (𝑧 = 𝑑 → (𝑧 = (𝐻𝑐) ↔ 𝑑 = (𝐻𝑐)))
79 sbceq1a 3750 . . . . . . . . . . . 12 (𝑧 = 𝑑 → (𝐺 We (𝑅1𝑐) ↔ [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
8078, 79imbi12d 344 . . . . . . . . . . 11 (𝑧 = 𝑑 → ((𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)) ↔ (𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐))))
8174, 77, 80cbvalv1 2337 . . . . . . . . . 10 (∀𝑧(𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)) ↔ ∀𝑑(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
8273, 81sylib 217 . . . . . . . . 9 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → ∀𝑑(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
83 nfsbc1v 3759 . . . . . . . . . 10 𝑑[(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐)
84 fnfun 6602 . . . . . . . . . . . 12 (𝐻 Fn On → Fun 𝐻)
8527, 84ax-mp 5 . . . . . . . . . . 11 Fun 𝐻
86 vex 3449 . . . . . . . . . . 11 𝑐 ∈ V
87 resfunexg 7165 . . . . . . . . . . 11 ((Fun 𝐻𝑐 ∈ V) → (𝐻𝑐) ∈ V)
8885, 86, 87mp2an 690 . . . . . . . . . 10 (𝐻𝑐) ∈ V
89 sbceq1a 3750 . . . . . . . . . 10 (𝑑 = (𝐻𝑐) → ([𝑑 / 𝑧]𝐺 We (𝑅1𝑐) ↔ [(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
9083, 88, 89ceqsal 3479 . . . . . . . . 9 (∀𝑑(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)) ↔ [(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐))
9182, 90sylib 217 . . . . . . . 8 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → [(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐))
92 sbccow 3762 . . . . . . . 8 ([(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐) ↔ [(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐))
9391, 92sylib 217 . . . . . . 7 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → [(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐))
94 nfcsb1v 3880 . . . . . . . . . 10 𝑧(𝐻𝑐) / 𝑧𝐺
95 nfcv 2907 . . . . . . . . . 10 𝑧(𝑅1𝑐)
9694, 95nfwe 5609 . . . . . . . . 9 𝑧(𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)
97 csbeq1a 3869 . . . . . . . . . 10 (𝑧 = (𝐻𝑐) → 𝐺 = (𝐻𝑐) / 𝑧𝐺)
98 weeq1 5621 . . . . . . . . . 10 (𝐺 = (𝐻𝑐) / 𝑧𝐺 → (𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
9997, 98syl 17 . . . . . . . . 9 (𝑧 = (𝐻𝑐) → (𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
10096, 99sbciegf 3778 . . . . . . . 8 ((𝐻𝑐) ∈ V → ([(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
10188, 100ax-mp 5 . . . . . . 7 ([(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐))
10293, 101sylib 217 . . . . . 6 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐))
103 recsval 8350 . . . . . . . . 9 (𝑐 ∈ On → (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)))
10426fveq1i 6843 . . . . . . . . 9 (𝐻𝑐) = (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐)
105 fvex 6855 . . . . . . . . . . . . . . 15 (𝑅1‘dom 𝑧) ∈ V
106105, 105xpex 7687 . . . . . . . . . . . . . 14 ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)) ∈ V
107106inex2 5275 . . . . . . . . . . . . 13 (if(dom 𝑧 = dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧))) ∈ V
10821, 107eqeltri 2834 . . . . . . . . . . . 12 𝐺 ∈ V
109108csbex 5268 . . . . . . . . . . 11 (𝐻𝑐) / 𝑧𝐺 ∈ V
110 eqid 2736 . . . . . . . . . . . 12 (𝑧 ∈ V ↦ 𝐺) = (𝑧 ∈ V ↦ 𝐺)
111110fvmpts 6951 . . . . . . . . . . 11 (((𝐻𝑐) ∈ V ∧ (𝐻𝑐) / 𝑧𝐺 ∈ V) → ((𝑧 ∈ V ↦ 𝐺)‘(𝐻𝑐)) = (𝐻𝑐) / 𝑧𝐺)
11288, 109, 111mp2an 690 . . . . . . . . . 10 ((𝑧 ∈ V ↦ 𝐺)‘(𝐻𝑐)) = (𝐻𝑐) / 𝑧𝐺
11326reseq1i 5933 . . . . . . . . . . 11 (𝐻𝑐) = (recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)
114113fveq2i 6845 . . . . . . . . . 10 ((𝑧 ∈ V ↦ 𝐺)‘(𝐻𝑐)) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
115112, 114eqtr3i 2766 . . . . . . . . 9 (𝐻𝑐) / 𝑧𝐺 = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
116103, 104, 1153eqtr4g 2801 . . . . . . . 8 (𝑐 ∈ On → (𝐻𝑐) = (𝐻𝑐) / 𝑧𝐺)
117 weeq1 5621 . . . . . . . 8 ((𝐻𝑐) = (𝐻𝑐) / 𝑧𝐺 → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
118116, 117syl 17 . . . . . . 7 (𝑐 ∈ On → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
1191183ad2ant1 1133 . . . . . 6 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
120102, 119mpbird 256 . . . . 5 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → (𝐻𝑐) We (𝑅1𝑐))
1211203exp 1119 . . . 4 (𝑐 ∈ On → (∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) → ((𝜑𝑐𝐴) → (𝐻𝑐) We (𝑅1𝑐))))
1229, 15, 121tfis3 7794 . . 3 (𝐴 ∈ On → ((𝜑𝐴𝐴) → (𝐻𝐴) We (𝑅1𝐴)))
1233, 122mpcom 38 . 2 ((𝜑𝐴𝐴) → (𝐻𝐴) We (𝑅1𝐴))
1241, 123mpan2 689 1 (𝜑 → (𝐻𝐴) We (𝑅1𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087  wal 1539   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  [wsbc 3739  csb 3855  cdif 3907  cin 3909  wss 3910  c0 4282  ifcif 4486  𝒫 cpw 4560  {csn 4586   cuni 4865   cint 4907   class class class wbr 5105  {copab 5167  cmpt 5188   E cep 5536   We wwe 5587   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  Oncon0 6317  suc csuc 6319  Fun wfun 6490   Fn wfn 6491  cfv 6496  recscrecs 8316  Fincfn 8883  supcsup 9376  𝑅1cr1 9698  rankcrnk 9699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-map 8767  df-en 8884  df-fin 8887  df-sup 9378  df-r1 9700  df-rank 9701
This theorem is referenced by:  aomclem7  41373
  Copyright terms: Public domain W3C validator