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 37946
Description: Lemma for dfac11 37949. 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 3657 . 2 𝐴𝐴
2 aomclem6.a . . . 4 (𝜑𝐴 ∈ On)
32adantr 480 . . 3 ((𝜑𝐴𝐴) → 𝐴 ∈ On)
4 sseq1 3659 . . . . . 6 (𝑐 = 𝑑 → (𝑐𝐴𝑑𝐴))
54anbi2d 740 . . . . 5 (𝑐 = 𝑑 → ((𝜑𝑐𝐴) ↔ (𝜑𝑑𝐴)))
6 fveq2 6229 . . . . . 6 (𝑐 = 𝑑 → (𝐻𝑐) = (𝐻𝑑))
7 fveq2 6229 . . . . . 6 (𝑐 = 𝑑 → (𝑅1𝑐) = (𝑅1𝑑))
86, 7weeq12d 37927 . . . . 5 (𝑐 = 𝑑 → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑑) We (𝑅1𝑑)))
95, 8imbi12d 333 . . . 4 (𝑐 = 𝑑 → (((𝜑𝑐𝐴) → (𝐻𝑐) We (𝑅1𝑐)) ↔ ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑))))
10 sseq1 3659 . . . . . 6 (𝑐 = 𝐴 → (𝑐𝐴𝐴𝐴))
1110anbi2d 740 . . . . 5 (𝑐 = 𝐴 → ((𝜑𝑐𝐴) ↔ (𝜑𝐴𝐴)))
12 fveq2 6229 . . . . . 6 (𝑐 = 𝐴 → (𝐻𝑐) = (𝐻𝐴))
13 fveq2 6229 . . . . . 6 (𝑐 = 𝐴 → (𝑅1𝑐) = (𝑅1𝐴))
1412, 13weeq12d 37927 . . . . 5 (𝑐 = 𝐴 → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝐴) We (𝑅1𝐴)))
1511, 14imbi12d 333 . . . 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 5356 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝐻𝑐) → dom 𝑧 = dom (𝐻𝑐))
2322adantl 481 . . . . . . . . . . . . . . . 16 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧 = dom (𝐻𝑐))
24 simpl1 1084 . . . . . . . . . . . . . . . . 17 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝑐 ∈ On)
25 onss 7032 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ On → 𝑐 ⊆ On)
26 aomclem6.h . . . . . . . . . . . . . . . . . . 19 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))
2726tfr1 7538 . . . . . . . . . . . . . . . . . 18 𝐻 Fn On
28 fnssres 6042 . . . . . . . . . . . . . . . . . 18 ((𝐻 Fn On ∧ 𝑐 ⊆ On) → (𝐻𝑐) Fn 𝑐)
2927, 28mpan 706 . . . . . . . . . . . . . . . . 17 (𝑐 ⊆ On → (𝐻𝑐) Fn 𝑐)
30 fndm 6028 . . . . . . . . . . . . . . . . 17 ((𝐻𝑐) Fn 𝑐 → dom (𝐻𝑐) = 𝑐)
3124, 25, 29, 304syl 19 . . . . . . . . . . . . . . . 16 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom (𝐻𝑐) = 𝑐)
3223, 31eqtrd 2685 . . . . . . . . . . . . . . 15 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧 = 𝑐)
3332, 24eqeltrd 2730 . . . . . . . . . . . . . 14 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧 ∈ On)
3432eleq2d 2716 . . . . . . . . . . . . . . . . . 18 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝑎 ∈ dom 𝑧𝑎𝑐))
3534biimpa 500 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎𝑐)
36 simpll2 1121 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)))
37 simpl3l 1136 . . . . . . . . . . . . . . . . . 18 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝜑)
3837adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝜑)
39 onelss 5804 . . . . . . . . . . . . . . . . . . . 20 (dom 𝑧 ∈ On → (𝑎 ∈ dom 𝑧𝑎 ⊆ dom 𝑧))
4033, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝑎 ∈ dom 𝑧𝑎 ⊆ dom 𝑧))
4140imp 444 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ dom 𝑧)
42 simpl3r 1137 . . . . . . . . . . . . . . . . . . . 20 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝑐𝐴)
4332, 42eqsstrd 3672 . . . . . . . . . . . . . . . . . . 19 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧𝐴)
4443adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → dom 𝑧𝐴)
4541, 44sstrd 3646 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎𝐴)
46 sseq1 3659 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (𝑑𝐴𝑎𝐴))
4746anbi2d 740 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → ((𝜑𝑑𝐴) ↔ (𝜑𝑎𝐴)))
48 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (𝐻𝑑) = (𝐻𝑎))
49 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (𝑅1𝑑) = (𝑅1𝑎))
5048, 49weeq12d 37927 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → ((𝐻𝑑) We (𝑅1𝑑) ↔ (𝐻𝑎) We (𝑅1𝑎)))
5147, 50imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑎 → (((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ↔ ((𝜑𝑎𝐴) → (𝐻𝑎) We (𝑅1𝑎))))
5251rspcva 3338 . . . . . . . . . . . . . . . . . 18 ((𝑎𝑐 ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑))) → ((𝜑𝑎𝐴) → (𝐻𝑎) We (𝑅1𝑎)))
5352imp 444 . . . . . . . . . . . . . . . . 17 (((𝑎𝑐 ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑))) ∧ (𝜑𝑎𝐴)) → (𝐻𝑎) We (𝑅1𝑎))
5435, 36, 38, 45, 53syl22anc 1367 . . . . . . . . . . . . . . . 16 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝐻𝑎) We (𝑅1𝑎))
55 fveq1 6228 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐻𝑐) → (𝑧𝑎) = ((𝐻𝑐)‘𝑎))
5655ad2antlr 763 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧𝑎) = ((𝐻𝑐)‘𝑎))
57 fvres 6245 . . . . . . . . . . . . . . . . . . 19 (𝑎𝑐 → ((𝐻𝑐)‘𝑎) = (𝐻𝑎))
5835, 57syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝐻𝑐)‘𝑎) = (𝐻𝑎))
5956, 58eqtrd 2685 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧𝑎) = (𝐻𝑎))
60 weeq1 5131 . . . . . . . . . . . . . . . . 17 ((𝑧𝑎) = (𝐻𝑎) → ((𝑧𝑎) We (𝑅1𝑎) ↔ (𝐻𝑎) We (𝑅1𝑎)))
6159, 60syl 17 . . . . . . . . . . . . . . . 16 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝑧𝑎) We (𝑅1𝑎) ↔ (𝐻𝑎) We (𝑅1𝑎)))
6254, 61mpbird 247 . . . . . . . . . . . . . . 15 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧𝑎) We (𝑅1𝑎))
6362ralrimiva 2995 . . . . . . . . . . . . . 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 37945 . . . . . . . . . . . . 13 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝐺 We (𝑅1‘dom 𝑧))
6832fveq2d 6233 . . . . . . . . . . . . . 14 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝑅1‘dom 𝑧) = (𝑅1𝑐))
69 weeq2 5132 . . . . . . . . . . . . . 14 ((𝑅1‘dom 𝑧) = (𝑅1𝑐) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1𝑐)))
7068, 69syl 17 . . . . . . . . . . . . 13 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1𝑐)))
7167, 70mpbid 222 . . . . . . . . . . . 12 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝐺 We (𝑅1𝑐))
7271ex 449 . . . . . . . . . . 11 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → (𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)))
7372alrimiv 1895 . . . . . . . . . 10 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → ∀𝑧(𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)))
74 nfv 1883 . . . . . . . . . . 11 𝑑(𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐))
75 nfv 1883 . . . . . . . . . . . 12 𝑧 𝑑 = (𝐻𝑐)
76 nfsbc1v 3488 . . . . . . . . . . . 12 𝑧[𝑑 / 𝑧]𝐺 We (𝑅1𝑐)
7775, 76nfim 1865 . . . . . . . . . . 11 𝑧(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐))
78 eqeq1 2655 . . . . . . . . . . . 12 (𝑧 = 𝑑 → (𝑧 = (𝐻𝑐) ↔ 𝑑 = (𝐻𝑐)))
79 sbceq1a 3479 . . . . . . . . . . . 12 (𝑧 = 𝑑 → (𝐺 We (𝑅1𝑐) ↔ [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
8078, 79imbi12d 333 . . . . . . . . . . 11 (𝑧 = 𝑑 → ((𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)) ↔ (𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐))))
8174, 77, 80cbval 2307 . . . . . . . . . 10 (∀𝑧(𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)) ↔ ∀𝑑(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
8273, 81sylib 208 . . . . . . . . 9 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → ∀𝑑(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
83 nfsbc1v 3488 . . . . . . . . . 10 𝑑[(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐)
84 fnfun 6026 . . . . . . . . . . . 12 (𝐻 Fn On → Fun 𝐻)
8527, 84ax-mp 5 . . . . . . . . . . 11 Fun 𝐻
86 vex 3234 . . . . . . . . . . 11 𝑐 ∈ V
87 resfunexg 6520 . . . . . . . . . . 11 ((Fun 𝐻𝑐 ∈ V) → (𝐻𝑐) ∈ V)
8885, 86, 87mp2an 708 . . . . . . . . . 10 (𝐻𝑐) ∈ V
89 sbceq1a 3479 . . . . . . . . . 10 (𝑑 = (𝐻𝑐) → ([𝑑 / 𝑧]𝐺 We (𝑅1𝑐) ↔ [(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
9083, 88, 89ceqsal 3263 . . . . . . . . 9 (∀𝑑(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)) ↔ [(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐))
9182, 90sylib 208 . . . . . . . 8 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → [(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐))
92 sbcco 3491 . . . . . . . 8 ([(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐) ↔ [(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐))
9391, 92sylib 208 . . . . . . 7 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → [(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐))
94 nfcsb1v 3582 . . . . . . . . . 10 𝑧(𝐻𝑐) / 𝑧𝐺
95 nfcv 2793 . . . . . . . . . 10 𝑧(𝑅1𝑐)
9694, 95nfwe 5119 . . . . . . . . 9 𝑧(𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)
97 csbeq1a 3575 . . . . . . . . . 10 (𝑧 = (𝐻𝑐) → 𝐺 = (𝐻𝑐) / 𝑧𝐺)
98 weeq1 5131 . . . . . . . . . 10 (𝐺 = (𝐻𝑐) / 𝑧𝐺 → (𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
9997, 98syl 17 . . . . . . . . 9 (𝑧 = (𝐻𝑐) → (𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
10096, 99sbciegf 3500 . . . . . . . 8 ((𝐻𝑐) ∈ V → ([(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
10188, 100ax-mp 5 . . . . . . 7 ([(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐))
10293, 101sylib 208 . . . . . 6 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐))
103 recsval 7545 . . . . . . . . 9 (𝑐 ∈ On → (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)))
10426fveq1i 6230 . . . . . . . . 9 (𝐻𝑐) = (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐)
105 fvex 6239 . . . . . . . . . . . . . . 15 (𝑅1‘dom 𝑧) ∈ V
106105, 105xpex 7004 . . . . . . . . . . . . . 14 ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)) ∈ V
107106inex2 4833 . . . . . . . . . . . . 13 (if(dom 𝑧 = dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧))) ∈ V
10821, 107eqeltri 2726 . . . . . . . . . . . 12 𝐺 ∈ V
109108csbex 4826 . . . . . . . . . . 11 (𝐻𝑐) / 𝑧𝐺 ∈ V
110 eqid 2651 . . . . . . . . . . . 12 (𝑧 ∈ V ↦ 𝐺) = (𝑧 ∈ V ↦ 𝐺)
111110fvmpts 6324 . . . . . . . . . . 11 (((𝐻𝑐) ∈ V ∧ (𝐻𝑐) / 𝑧𝐺 ∈ V) → ((𝑧 ∈ V ↦ 𝐺)‘(𝐻𝑐)) = (𝐻𝑐) / 𝑧𝐺)
11288, 109, 111mp2an 708 . . . . . . . . . 10 ((𝑧 ∈ V ↦ 𝐺)‘(𝐻𝑐)) = (𝐻𝑐) / 𝑧𝐺
11326reseq1i 5424 . . . . . . . . . . 11 (𝐻𝑐) = (recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)
114113fveq2i 6232 . . . . . . . . . 10 ((𝑧 ∈ V ↦ 𝐺)‘(𝐻𝑐)) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
115112, 114eqtr3i 2675 . . . . . . . . 9 (𝐻𝑐) / 𝑧𝐺 = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
116103, 104, 1153eqtr4g 2710 . . . . . . . 8 (𝑐 ∈ On → (𝐻𝑐) = (𝐻𝑐) / 𝑧𝐺)
117 weeq1 5131 . . . . . . . 8 ((𝐻𝑐) = (𝐻𝑐) / 𝑧𝐺 → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
118116, 117syl 17 . . . . . . 7 (𝑐 ∈ On → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
1191183ad2ant1 1102 . . . . . 6 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
120102, 119mpbird 247 . . . . 5 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → (𝐻𝑐) We (𝑅1𝑐))
1211203exp 1283 . . . 4 (𝑐 ∈ On → (∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) → ((𝜑𝑐𝐴) → (𝐻𝑐) We (𝑅1𝑐))))
1229, 15, 121tfis3 7099 . . 3 (𝐴 ∈ On → ((𝜑𝐴𝐴) → (𝐻𝐴) We (𝑅1𝐴)))
1233, 122mpcom 38 . 2 ((𝜑𝐴𝐴) → (𝐻𝐴) We (𝑅1𝐴))
1241, 123mpan2 707 1 (𝜑 → (𝐻𝐴) We (𝑅1𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054  wal 1521   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  [wsbc 3468  csb 3566  cdif 3604  cin 3606  wss 3607  c0 3948  ifcif 4119  𝒫 cpw 4191  {csn 4210   cuni 4468   cint 4507   class class class wbr 4685  {copab 4745  cmpt 4762   E cep 5057   We wwe 5101   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  Oncon0 5761  suc csuc 5763  Fun wfun 5920   Fn wfn 5921  cfv 5926  recscrecs 7512  Fincfn 7997  supcsup 8387  𝑅1cr1 8663  rankcrnk 8664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-er 7787  df-map 7901  df-en 7998  df-fin 8001  df-sup 8389  df-r1 8665  df-rank 8666
This theorem is referenced by:  aomclem7  37947
  Copyright terms: Public domain W3C validator