MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttukeylem6 Structured version   Visualization version   GIF version

Theorem ttukeylem6 9928
Description: Lemma for ttukey 9932. (Contributed by Mario Carneiro, 15-May-2015.)
Hypotheses
Ref Expression
ttukeylem.1 (𝜑𝐹:(card‘( 𝐴𝐵))–1-1-onto→( 𝐴𝐵))
ttukeylem.2 (𝜑𝐵𝐴)
ttukeylem.3 (𝜑 → ∀𝑥(𝑥𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴))
ttukeylem.4 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅)))))
Assertion
Ref Expression
ttukeylem6 ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → (𝐺𝐶) ∈ 𝐴)
Distinct variable groups:   𝑥,𝑧,𝐶   𝑥,𝐺,𝑧   𝜑,𝑧   𝑥,𝐴,𝑧   𝑥,𝐵,𝑧   𝑥,𝐹,𝑧
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ttukeylem6
Dummy variables 𝑎 𝑦 𝑓 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cardon 9365 . . . . 5 (card‘( 𝐴𝐵)) ∈ On
21onsuci 7545 . . . 4 suc (card‘( 𝐴𝐵)) ∈ On
32a1i 11 . . 3 (𝜑 → suc (card‘( 𝐴𝐵)) ∈ On)
4 onelon 6209 . . 3 ((suc (card‘( 𝐴𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘( 𝐴𝐵))) → 𝐶 ∈ On)
53, 4sylan 582 . 2 ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → 𝐶 ∈ On)
6 eleq1 2898 . . . . . 6 (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) ↔ 𝑎 ∈ suc (card‘( 𝐴𝐵))))
7 fveq2 6663 . . . . . . 7 (𝑦 = 𝑎 → (𝐺𝑦) = (𝐺𝑎))
87eleq1d 2895 . . . . . 6 (𝑦 = 𝑎 → ((𝐺𝑦) ∈ 𝐴 ↔ (𝐺𝑎) ∈ 𝐴))
96, 8imbi12d 347 . . . . 5 (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
109imbi2d 343 . . . 4 (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴))))
11 eleq1 2898 . . . . . 6 (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) ↔ 𝐶 ∈ suc (card‘( 𝐴𝐵))))
12 fveq2 6663 . . . . . . 7 (𝑦 = 𝐶 → (𝐺𝑦) = (𝐺𝐶))
1312eleq1d 2895 . . . . . 6 (𝑦 = 𝐶 → ((𝐺𝑦) ∈ 𝐴 ↔ (𝐺𝐶) ∈ 𝐴))
1411, 13imbi12d 347 . . . . 5 (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝐶) ∈ 𝐴)))
1514imbi2d 343 . . . 4 (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝐶) ∈ 𝐴))))
16 r19.21v 3173 . . . . . 6 (∀𝑎𝑦 (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
172onordi 6288 . . . . . . . . . . . . . . 15 Ord suc (card‘( 𝐴𝐵))
1817a1i 11 . . . . . . . . . . . . . 14 (𝜑 → Ord suc (card‘( 𝐴𝐵)))
19 ordelss 6200 . . . . . . . . . . . . . 14 ((Ord suc (card‘( 𝐴𝐵)) ∧ 𝑦 ∈ suc (card‘( 𝐴𝐵))) → 𝑦 ⊆ suc (card‘( 𝐴𝐵)))
2018, 19sylan 582 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → 𝑦 ⊆ suc (card‘( 𝐴𝐵)))
2120sselda 3965 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) ∧ 𝑎𝑦) → 𝑎 ∈ suc (card‘( 𝐴𝐵)))
22 biimt 363 . . . . . . . . . . . 12 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → ((𝐺𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
2321, 22syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) ∧ 𝑎𝑦) → ((𝐺𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
2423ralbidva 3194 . . . . . . . . . 10 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → (∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴 ↔ ∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
252onssi 7544 . . . . . . . . . . . . . 14 suc (card‘( 𝐴𝐵)) ⊆ On
26 simprl 769 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘( 𝐴𝐵)))
2725, 26sseldi 3963 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → 𝑦 ∈ On)
28 ttukeylem.1 . . . . . . . . . . . . . 14 (𝜑𝐹:(card‘( 𝐴𝐵))–1-1-onto→( 𝐴𝐵))
29 ttukeylem.2 . . . . . . . . . . . . . 14 (𝜑𝐵𝐴)
30 ttukeylem.3 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥(𝑥𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴))
31 ttukeylem.4 . . . . . . . . . . . . . 14 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅)))))
3228, 29, 30, 31ttukeylem3 9925 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ On) → (𝐺𝑦) = if(𝑦 = 𝑦, if(𝑦 = ∅, 𝐵, (𝐺𝑦)), ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅))))
3327, 32syldan 593 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → (𝐺𝑦) = if(𝑦 = 𝑦, if(𝑦 = ∅, 𝐵, (𝐺𝑦)), ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅))))
3429ad3antrrr 728 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑦 = ∅) → 𝐵𝐴)
35 simpr 487 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin))
3635elin2d 4174 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
3735elin1d 4173 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 ∈ 𝒫 (𝐺𝑦))
3837elpwid 4551 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 (𝐺𝑦))
3931tfr1 8025 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 Fn On
40 fnfun 6446 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn On → Fun 𝐺)
41 funiunfv 6999 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐺 𝑣𝑦 (𝐺𝑣) = (𝐺𝑦))
4239, 40, 41mp2b 10 . . . . . . . . . . . . . . . . . . . . . 22 𝑣𝑦 (𝐺𝑣) = (𝐺𝑦)
4338, 42sseqtrrdi 4016 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 𝑣𝑦 (𝐺𝑣))
44 dfss3 3954 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 𝑣𝑦 (𝐺𝑣) ↔ ∀𝑢𝑤 𝑢 𝑣𝑦 (𝐺𝑣))
45 eliun 4914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 𝑣𝑦 (𝐺𝑣) ↔ ∃𝑣𝑦 𝑢 ∈ (𝐺𝑣))
4645ralbii 3163 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑢𝑤 𝑢 𝑣𝑦 (𝐺𝑣) ↔ ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣))
4744, 46bitri 277 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 𝑣𝑦 (𝐺𝑣) ↔ ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣))
4843, 47sylib 220 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣))
49 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (𝑓𝑢) → (𝐺𝑣) = (𝐺‘(𝑓𝑢)))
5049eleq2d 2896 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (𝑓𝑢) → (𝑢 ∈ (𝐺𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓𝑢))))
5150ac6sfi 8754 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 ∈ Fin ∧ ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣)) → ∃𝑓(𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))
5236, 48, 51syl2anc 586 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ∃𝑓(𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))
53 eleq1 2898 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = ∅ → (𝑤𝐴 ↔ ∅ ∈ 𝐴))
54 simp-4l 781 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑)
55 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = ran 𝑓 → (𝐺𝑎) = (𝐺 ran 𝑓))
5655eleq1d 2895 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = ran 𝑓 → ((𝐺𝑎) ∈ 𝐴 ↔ (𝐺 ran 𝑓) ∈ 𝐴))
57 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)
5857ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)
59 simprrl 779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → 𝑓:𝑤𝑦)
6059adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤𝑦)
61 frn 6513 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑤𝑦 → ran 𝑓𝑦)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓𝑦)
6327ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On)
64 onss 7497 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ On → 𝑦 ⊆ On)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On)
6662, 65sstrd 3975 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ On)
6736adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → 𝑤 ∈ Fin)
6867adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ Fin)
69 ffn 6507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:𝑤𝑦𝑓 Fn 𝑤)
7060, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤)
71 dffn4 6589 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 Fn 𝑤𝑓:𝑤onto→ran 𝑓)
7270, 71sylib 220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤onto→ran 𝑓)
73 fofi 8802 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤 ∈ Fin ∧ 𝑓:𝑤onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7468, 72, 73syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin)
75 dm0rn0 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
7659fdmd 6516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → dom 𝑓 = 𝑤)
7776eqeq1d 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → (dom 𝑓 = ∅ ↔ 𝑤 = ∅))
7875, 77syl5bbr 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → (ran 𝑓 = ∅ ↔ 𝑤 = ∅))
7978necon3bid 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅))
8079biimpar 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅)
81 ordunifi 8760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran 𝑓 ⊆ On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ∈ ran 𝑓)
8266, 74, 80, 81syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ ran 𝑓)
8362, 82sseldd 3966 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓𝑦)
8456, 58, 83rspcdva 3623 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → (𝐺 ran 𝑓) ∈ 𝐴)
85 simp-4l 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝜑)
8627ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑦 ∈ On)
8786, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑦 ⊆ On)
88 ffvelrn 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓:𝑤𝑦𝑢𝑤) → (𝑓𝑢) ∈ 𝑦)
8988adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ∈ 𝑦)
9087, 89sseldd 3966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ∈ On)
9161ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → ran 𝑓𝑦)
9291, 87sstrd 3975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → ran 𝑓 ⊆ On)
93 vex 3496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑓 ∈ V
9493rnex 7609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran 𝑓 ∈ V
9594ssonunii 7494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ran 𝑓 ⊆ On → ran 𝑓 ∈ On)
9692, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → ran 𝑓 ∈ On)
9769ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑓 Fn 𝑤)
98 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑢𝑤)
99 fnfvelrn 6841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 Fn 𝑤𝑢𝑤) → (𝑓𝑢) ∈ ran 𝑓)
10097, 98, 99syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ∈ ran 𝑓)
101 elssuni 4859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓𝑢) ∈ ran 𝑓 → (𝑓𝑢) ⊆ ran 𝑓)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ⊆ ran 𝑓)
10328, 29, 30, 31ttukeylem5 9927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ ((𝑓𝑢) ∈ On ∧ ran 𝑓 ∈ On ∧ (𝑓𝑢) ⊆ ran 𝑓)) → (𝐺‘(𝑓𝑢)) ⊆ (𝐺 ran 𝑓))
10485, 90, 96, 102, 103syl13anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝐺‘(𝑓𝑢)) ⊆ (𝐺 ran 𝑓))
105104sseld 3964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑢 ∈ (𝐺‘(𝑓𝑢)) → 𝑢 ∈ (𝐺 ran 𝑓)))
106105anassrs 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ 𝑓:𝑤𝑦) ∧ 𝑢𝑤) → (𝑢 ∈ (𝐺‘(𝑓𝑢)) → 𝑢 ∈ (𝐺 ran 𝑓)))
107106ralimdva 3175 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ 𝑓:𝑤𝑦) → (∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢)) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓)))
108107expimpd 456 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ((𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓)))
109108impr 457 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓))
110109adantr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓))
111 dfss3 3954 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ⊆ (𝐺 ran 𝑓) ↔ ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓))
112110, 111sylibr 236 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺 ran 𝑓))
11328, 29, 30ttukeylem2 9924 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝐺 ran 𝑓) ∈ 𝐴𝑤 ⊆ (𝐺 ran 𝑓))) → 𝑤𝐴)
11454, 84, 112, 113syl12anc 834 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤𝐴)
115 0ss 4348 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∅ ⊆ 𝐵
11628, 29, 30ttukeylem2 9924 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐵𝐴 ∧ ∅ ⊆ 𝐵)) → ∅ ∈ 𝐴)
117115, 116mpanr2 702 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝐵𝐴) → ∅ ∈ 𝐴)
11829, 117mpdan 685 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∅ ∈ 𝐴)
119118ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → ∅ ∈ 𝐴)
12053, 114, 119pm2.61ne 3100 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → 𝑤𝐴)
121120expr 459 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ((𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))) → 𝑤𝐴))
122121exlimdv 1927 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → (∃𝑓(𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))) → 𝑤𝐴))
12352, 122mpd 15 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤𝐴)
124123ex 415 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) → 𝑤𝐴))
125124ssrdv 3971 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝐴)
12628, 29, 30ttukeylem1 9923 . . . . . . . . . . . . . . . . 17 (𝜑 → ( (𝐺𝑦) ∈ 𝐴 ↔ (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝐴))
127126ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → ( (𝐺𝑦) ∈ 𝐴 ↔ (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝐴))
128125, 127mpbird 259 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → (𝐺𝑦) ∈ 𝐴)
129128adantr 483 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ ¬ 𝑦 = ∅) → (𝐺𝑦) ∈ 𝐴)
13034, 129ifclda 4499 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → if(𝑦 = ∅, 𝐵, (𝐺𝑦)) ∈ 𝐴)
131 uneq2 4131 . . . . . . . . . . . . . . 15 ({(𝐹 𝑦)} = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) = ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)))
132131eleq1d 2895 . . . . . . . . . . . . . 14 ({(𝐹 𝑦)} = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → (((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴 ↔ ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)) ∈ 𝐴))
133 un0 4342 . . . . . . . . . . . . . . . 16 ((𝐺 𝑦) ∪ ∅) = (𝐺 𝑦)
134 uneq2 4131 . . . . . . . . . . . . . . . 16 (∅ = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → ((𝐺 𝑦) ∪ ∅) = ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)))
135133, 134syl5eqr 2868 . . . . . . . . . . . . . . 15 (∅ = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → (𝐺 𝑦) = ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)))
136135eleq1d 2895 . . . . . . . . . . . . . 14 (∅ = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → ((𝐺 𝑦) ∈ 𝐴 ↔ ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)) ∈ 𝐴))
137 simpr 487 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) ∧ ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴) → ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴)
138 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑦 → (𝐺𝑎) = (𝐺 𝑦))
139138eleq1d 2895 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑦 → ((𝐺𝑎) ∈ 𝐴 ↔ (𝐺 𝑦) ∈ 𝐴))
140 simplrr 776 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)
141 vuniex 7457 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
142141sucid 6263 . . . . . . . . . . . . . . . . 17 𝑦 ∈ suc 𝑦
143 eloni 6194 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On → Ord 𝑦)
144 orduniorsuc 7537 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 → (𝑦 = 𝑦𝑦 = suc 𝑦))
14527, 143, 1443syl 18 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → (𝑦 = 𝑦𝑦 = suc 𝑦))
146145orcanai 998 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → 𝑦 = suc 𝑦)
147142, 146eleqtrrid 2918 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → 𝑦𝑦)
148139, 140, 147rspcdva 3623 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → (𝐺 𝑦) ∈ 𝐴)
149148adantr 483 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) ∧ ¬ ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴) → (𝐺 𝑦) ∈ 𝐴)
150132, 136, 137, 149ifbothda 4502 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)) ∈ 𝐴)
151130, 150ifclda 4499 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → if(𝑦 = 𝑦, if(𝑦 = ∅, 𝐵, (𝐺𝑦)), ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅))) ∈ 𝐴)
15233, 151eqeltrd 2911 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → (𝐺𝑦) ∈ 𝐴)
153152expr 459 . . . . . . . . . 10 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → (∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴 → (𝐺𝑦) ∈ 𝐴))
15424, 153sylbird 262 . . . . . . . . 9 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → (∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴))
155154ex 415 . . . . . . . 8 (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴)))
156155com23 86 . . . . . . 7 (𝜑 → (∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴) → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)))
157156a2i 14 . . . . . 6 ((𝜑 → ∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)))
15816, 157sylbi 219 . . . . 5 (∀𝑎𝑦 (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)))
159158a1i 11 . . . 4 (𝑦 ∈ On → (∀𝑎𝑦 (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴))))
16010, 15, 159tfis3 7564 . . 3 (𝐶 ∈ On → (𝜑 → (𝐶 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝐶) ∈ 𝐴)))
161160impd 413 . 2 (𝐶 ∈ On → ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → (𝐺𝐶) ∈ 𝐴))
1625, 161mpcom 38 1 ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → (𝐺𝐶) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  wal 1528   = wceq 1530  wex 1773  wcel 2107  wne 3014  wral 3136  wrex 3137  Vcvv 3493  cdif 3931  cun 3932  cin 3933  wss 3934  c0 4289  ifcif 4465  𝒫 cpw 4537  {csn 4559   cuni 4830   ciun 4910  cmpt 5137  dom cdm 5548  ran crn 5549  cima 5551  Ord word 6183  Oncon0 6184  suc csuc 6186  Fun wfun 6342   Fn wfn 6343  wf 6344  ontowfo 6346  1-1-ontowf1o 6347  cfv 6348  recscrecs 7999  Fincfn 8501  cardccrd 9356
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-om 7573  df-wrecs 7939  df-recs 8000  df-1o 8094  df-er 8281  df-en 8502  df-dom 8503  df-fin 8505  df-card 9360
This theorem is referenced by:  ttukeylem7  9929
  Copyright terms: Public domain W3C validator