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 40174
 Description: Lemma for dfac11 40177. 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 3939 . 2 𝐴𝐴
2 aomclem6.a . . . 4 (𝜑𝐴 ∈ On)
32adantr 484 . . 3 ((𝜑𝐴𝐴) → 𝐴 ∈ On)
4 sseq1 3942 . . . . . 6 (𝑐 = 𝑑 → (𝑐𝐴𝑑𝐴))
54anbi2d 631 . . . . 5 (𝑐 = 𝑑 → ((𝜑𝑐𝐴) ↔ (𝜑𝑑𝐴)))
6 fveq2 6655 . . . . . 6 (𝑐 = 𝑑 → (𝐻𝑐) = (𝐻𝑑))
7 fveq2 6655 . . . . . 6 (𝑐 = 𝑑 → (𝑅1𝑐) = (𝑅1𝑑))
86, 7weeq12d 40155 . . . . 5 (𝑐 = 𝑑 → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑑) We (𝑅1𝑑)))
95, 8imbi12d 348 . . . 4 (𝑐 = 𝑑 → (((𝜑𝑐𝐴) → (𝐻𝑐) We (𝑅1𝑐)) ↔ ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑))))
10 sseq1 3942 . . . . . 6 (𝑐 = 𝐴 → (𝑐𝐴𝐴𝐴))
1110anbi2d 631 . . . . 5 (𝑐 = 𝐴 → ((𝜑𝑐𝐴) ↔ (𝜑𝐴𝐴)))
12 fveq2 6655 . . . . . 6 (𝑐 = 𝐴 → (𝐻𝑐) = (𝐻𝐴))
13 fveq2 6655 . . . . . 6 (𝑐 = 𝐴 → (𝑅1𝑐) = (𝑅1𝐴))
1412, 13weeq12d 40155 . . . . 5 (𝑐 = 𝐴 → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝐴) We (𝑅1𝐴)))
1511, 14imbi12d 348 . . . 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 5742 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝐻𝑐) → dom 𝑧 = dom (𝐻𝑐))
2322adantl 485 . . . . . . . . . . . . . . . 16 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧 = dom (𝐻𝑐))
24 simpl1 1188 . . . . . . . . . . . . . . . . 17 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝑐 ∈ On)
25 onss 7498 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ On → 𝑐 ⊆ On)
26 aomclem6.h . . . . . . . . . . . . . . . . . . 19 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))
2726tfr1 8034 . . . . . . . . . . . . . . . . . 18 𝐻 Fn On
28 fnssres 6450 . . . . . . . . . . . . . . . . . 18 ((𝐻 Fn On ∧ 𝑐 ⊆ On) → (𝐻𝑐) Fn 𝑐)
2927, 28mpan 689 . . . . . . . . . . . . . . . . 17 (𝑐 ⊆ On → (𝐻𝑐) Fn 𝑐)
30 fndm 6433 . . . . . . . . . . . . . . . . 17 ((𝐻𝑐) Fn 𝑐 → dom (𝐻𝑐) = 𝑐)
3124, 25, 29, 304syl 19 . . . . . . . . . . . . . . . 16 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom (𝐻𝑐) = 𝑐)
3223, 31eqtrd 2833 . . . . . . . . . . . . . . 15 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧 = 𝑐)
3332, 24eqeltrd 2890 . . . . . . . . . . . . . 14 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧 ∈ On)
3432eleq2d 2875 . . . . . . . . . . . . . . . . . 18 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝑎 ∈ dom 𝑧𝑎𝑐))
3534biimpa 480 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎𝑐)
36 simpll2 1210 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)))
37 simpl3l 1225 . . . . . . . . . . . . . . . . . 18 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝜑)
3837adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝜑)
39 onelss 6208 . . . . . . . . . . . . . . . . . . . 20 (dom 𝑧 ∈ On → (𝑎 ∈ dom 𝑧𝑎 ⊆ dom 𝑧))
4033, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝑎 ∈ dom 𝑧𝑎 ⊆ dom 𝑧))
4140imp 410 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ dom 𝑧)
42 simpl3r 1226 . . . . . . . . . . . . . . . . . . . 20 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝑐𝐴)
4332, 42eqsstrd 3955 . . . . . . . . . . . . . . . . . . 19 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → dom 𝑧𝐴)
4443adantr 484 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → dom 𝑧𝐴)
4541, 44sstrd 3927 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎𝐴)
46 sseq1 3942 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (𝑑𝐴𝑎𝐴))
4746anbi2d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → ((𝜑𝑑𝐴) ↔ (𝜑𝑎𝐴)))
48 fveq2 6655 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (𝐻𝑑) = (𝐻𝑎))
49 fveq2 6655 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (𝑅1𝑑) = (𝑅1𝑎))
5048, 49weeq12d 40155 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → ((𝐻𝑑) We (𝑅1𝑑) ↔ (𝐻𝑎) We (𝑅1𝑎)))
5147, 50imbi12d 348 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑎 → (((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ↔ ((𝜑𝑎𝐴) → (𝐻𝑎) We (𝑅1𝑎))))
5251rspcva 3570 . . . . . . . . . . . . . . . . . 18 ((𝑎𝑐 ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑))) → ((𝜑𝑎𝐴) → (𝐻𝑎) We (𝑅1𝑎)))
5352imp 410 . . . . . . . . . . . . . . . . 17 (((𝑎𝑐 ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑))) ∧ (𝜑𝑎𝐴)) → (𝐻𝑎) We (𝑅1𝑎))
5435, 36, 38, 45, 53syl22anc 837 . . . . . . . . . . . . . . . 16 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝐻𝑎) We (𝑅1𝑎))
55 fveq1 6654 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐻𝑐) → (𝑧𝑎) = ((𝐻𝑐)‘𝑎))
5655ad2antlr 726 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧𝑎) = ((𝐻𝑐)‘𝑎))
57 fvres 6674 . . . . . . . . . . . . . . . . . . 19 (𝑎𝑐 → ((𝐻𝑐)‘𝑎) = (𝐻𝑎))
5835, 57syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝐻𝑐)‘𝑎) = (𝐻𝑎))
5956, 58eqtrd 2833 . . . . . . . . . . . . . . . . 17 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧𝑎) = (𝐻𝑎))
60 weeq1 5511 . . . . . . . . . . . . . . . . 17 ((𝑧𝑎) = (𝐻𝑎) → ((𝑧𝑎) We (𝑅1𝑎) ↔ (𝐻𝑎) We (𝑅1𝑎)))
6159, 60syl 17 . . . . . . . . . . . . . . . 16 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝑧𝑎) We (𝑅1𝑎) ↔ (𝐻𝑎) We (𝑅1𝑎)))
6254, 61mpbird 260 . . . . . . . . . . . . . . 15 ((((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧𝑎) We (𝑅1𝑎))
6362ralrimiva 3149 . . . . . . . . . . . . . 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 40173 . . . . . . . . . . . . 13 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝐺 We (𝑅1‘dom 𝑧))
6832fveq2d 6659 . . . . . . . . . . . . . 14 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝑅1‘dom 𝑧) = (𝑅1𝑐))
69 weeq2 5512 . . . . . . . . . . . . . 14 ((𝑅1‘dom 𝑧) = (𝑅1𝑐) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1𝑐)))
7068, 69syl 17 . . . . . . . . . . . . 13 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1𝑐)))
7167, 70mpbid 235 . . . . . . . . . . . 12 (((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) ∧ 𝑧 = (𝐻𝑐)) → 𝐺 We (𝑅1𝑐))
7271ex 416 . . . . . . . . . . 11 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → (𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)))
7372alrimiv 1928 . . . . . . . . . 10 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → ∀𝑧(𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)))
74 nfv 1915 . . . . . . . . . . 11 𝑑(𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐))
75 nfv 1915 . . . . . . . . . . . 12 𝑧 𝑑 = (𝐻𝑐)
76 nfsbc1v 3742 . . . . . . . . . . . 12 𝑧[𝑑 / 𝑧]𝐺 We (𝑅1𝑐)
7775, 76nfim 1897 . . . . . . . . . . 11 𝑧(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐))
78 eqeq1 2802 . . . . . . . . . . . 12 (𝑧 = 𝑑 → (𝑧 = (𝐻𝑐) ↔ 𝑑 = (𝐻𝑐)))
79 sbceq1a 3733 . . . . . . . . . . . 12 (𝑧 = 𝑑 → (𝐺 We (𝑅1𝑐) ↔ [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
8078, 79imbi12d 348 . . . . . . . . . . 11 (𝑧 = 𝑑 → ((𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)) ↔ (𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐))))
8174, 77, 80cbvalv1 2350 . . . . . . . . . 10 (∀𝑧(𝑧 = (𝐻𝑐) → 𝐺 We (𝑅1𝑐)) ↔ ∀𝑑(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
8273, 81sylib 221 . . . . . . . . 9 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → ∀𝑑(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
83 nfsbc1v 3742 . . . . . . . . . 10 𝑑[(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐)
84 fnfun 6431 . . . . . . . . . . . 12 (𝐻 Fn On → Fun 𝐻)
8527, 84ax-mp 5 . . . . . . . . . . 11 Fun 𝐻
86 vex 3445 . . . . . . . . . . 11 𝑐 ∈ V
87 resfunexg 6965 . . . . . . . . . . 11 ((Fun 𝐻𝑐 ∈ V) → (𝐻𝑐) ∈ V)
8885, 86, 87mp2an 691 . . . . . . . . . 10 (𝐻𝑐) ∈ V
89 sbceq1a 3733 . . . . . . . . . 10 (𝑑 = (𝐻𝑐) → ([𝑑 / 𝑧]𝐺 We (𝑅1𝑐) ↔ [(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐)))
9083, 88, 89ceqsal 3479 . . . . . . . . 9 (∀𝑑(𝑑 = (𝐻𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1𝑐)) ↔ [(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐))
9182, 90sylib 221 . . . . . . . 8 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → [(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐))
92 sbccow 3745 . . . . . . . 8 ([(𝐻𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1𝑐) ↔ [(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐))
9391, 92sylib 221 . . . . . . 7 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → [(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐))
94 nfcsb1v 3854 . . . . . . . . . 10 𝑧(𝐻𝑐) / 𝑧𝐺
95 nfcv 2955 . . . . . . . . . 10 𝑧(𝑅1𝑐)
9694, 95nfwe 5499 . . . . . . . . 9 𝑧(𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)
97 csbeq1a 3844 . . . . . . . . . 10 (𝑧 = (𝐻𝑐) → 𝐺 = (𝐻𝑐) / 𝑧𝐺)
98 weeq1 5511 . . . . . . . . . 10 (𝐺 = (𝐻𝑐) / 𝑧𝐺 → (𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
9997, 98syl 17 . . . . . . . . 9 (𝑧 = (𝐻𝑐) → (𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
10096, 99sbciegf 3759 . . . . . . . 8 ((𝐻𝑐) ∈ V → ([(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
10188, 100ax-mp 5 . . . . . . 7 ([(𝐻𝑐) / 𝑧]𝐺 We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐))
10293, 101sylib 221 . . . . . 6 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐))
103 recsval 8041 . . . . . . . . 9 (𝑐 ∈ On → (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)))
10426fveq1i 6656 . . . . . . . . 9 (𝐻𝑐) = (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐)
105 fvex 6668 . . . . . . . . . . . . . . 15 (𝑅1‘dom 𝑧) ∈ V
106105, 105xpex 7469 . . . . . . . . . . . . . 14 ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)) ∈ V
107106inex2 5190 . . . . . . . . . . . . 13 (if(dom 𝑧 = dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧))) ∈ V
10821, 107eqeltri 2886 . . . . . . . . . . . 12 𝐺 ∈ V
109108csbex 5183 . . . . . . . . . . 11 (𝐻𝑐) / 𝑧𝐺 ∈ V
110 eqid 2798 . . . . . . . . . . . 12 (𝑧 ∈ V ↦ 𝐺) = (𝑧 ∈ V ↦ 𝐺)
111110fvmpts 6758 . . . . . . . . . . 11 (((𝐻𝑐) ∈ V ∧ (𝐻𝑐) / 𝑧𝐺 ∈ V) → ((𝑧 ∈ V ↦ 𝐺)‘(𝐻𝑐)) = (𝐻𝑐) / 𝑧𝐺)
11288, 109, 111mp2an 691 . . . . . . . . . 10 ((𝑧 ∈ V ↦ 𝐺)‘(𝐻𝑐)) = (𝐻𝑐) / 𝑧𝐺
11326reseq1i 5818 . . . . . . . . . . 11 (𝐻𝑐) = (recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)
114113fveq2i 6658 . . . . . . . . . 10 ((𝑧 ∈ V ↦ 𝐺)‘(𝐻𝑐)) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
115112, 114eqtr3i 2823 . . . . . . . . 9 (𝐻𝑐) / 𝑧𝐺 = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
116103, 104, 1153eqtr4g 2858 . . . . . . . 8 (𝑐 ∈ On → (𝐻𝑐) = (𝐻𝑐) / 𝑧𝐺)
117 weeq1 5511 . . . . . . . 8 ((𝐻𝑐) = (𝐻𝑐) / 𝑧𝐺 → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
118116, 117syl 17 . . . . . . 7 (𝑐 ∈ On → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
1191183ad2ant1 1130 . . . . . 6 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → ((𝐻𝑐) We (𝑅1𝑐) ↔ (𝐻𝑐) / 𝑧𝐺 We (𝑅1𝑐)))
120102, 119mpbird 260 . . . . 5 ((𝑐 ∈ On ∧ ∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) ∧ (𝜑𝑐𝐴)) → (𝐻𝑐) We (𝑅1𝑐))
1211203exp 1116 . . . 4 (𝑐 ∈ On → (∀𝑑𝑐 ((𝜑𝑑𝐴) → (𝐻𝑑) We (𝑅1𝑑)) → ((𝜑𝑐𝐴) → (𝐻𝑐) We (𝑅1𝑐))))
1229, 15, 121tfis3 7565 . . 3 (𝐴 ∈ On → ((𝜑𝐴𝐴) → (𝐻𝐴) We (𝑅1𝐴)))
1233, 122mpcom 38 . 2 ((𝜑𝐴𝐴) → (𝐻𝐴) We (𝑅1𝐴))
1241, 123mpan2 690 1 (𝜑 → (𝐻𝐴) We (𝑅1𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3442  [wsbc 3722  ⦋csb 3830   ∖ cdif 3880   ∩ cin 3882   ⊆ wss 3883  ∅c0 4246  ifcif 4428  𝒫 cpw 4500  {csn 4528  ∪ cuni 4804  ∩ cint 4842   class class class wbr 5034  {copab 5096   ↦ cmpt 5114   E cep 5433   We wwe 5481   × cxp 5521  ◡ccnv 5522  dom cdm 5523  ran crn 5524   ↾ cres 5525   “ cima 5526  Oncon0 6166  suc csuc 6168  Fun wfun 6326   Fn wfn 6327  ‘cfv 6332  recscrecs 8008  Fincfn 8510  supcsup 8906  𝑅1cr1 9193  rankcrnk 9194 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-2o 8104  df-er 8290  df-map 8409  df-en 8511  df-fin 8514  df-sup 8908  df-r1 9195  df-rank 9196 This theorem is referenced by:  aomclem7  40175
 Copyright terms: Public domain W3C validator