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

Theorem ttukeylem6 9591
Description: Lemma for ttukey 9595. (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 9023 . . . . 5 (card‘( 𝐴𝐵)) ∈ On
21onsuci 7238 . . . 4 suc (card‘( 𝐴𝐵)) ∈ On
32a1i 11 . . 3 (𝜑 → suc (card‘( 𝐴𝐵)) ∈ On)
4 onelon 5935 . . 3 ((suc (card‘( 𝐴𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘( 𝐴𝐵))) → 𝐶 ∈ On)
53, 4sylan 575 . 2 ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → 𝐶 ∈ On)
6 eleq1 2832 . . . . . 6 (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) ↔ 𝑎 ∈ suc (card‘( 𝐴𝐵))))
7 fveq2 6377 . . . . . . 7 (𝑦 = 𝑎 → (𝐺𝑦) = (𝐺𝑎))
87eleq1d 2829 . . . . . 6 (𝑦 = 𝑎 → ((𝐺𝑦) ∈ 𝐴 ↔ (𝐺𝑎) ∈ 𝐴))
96, 8imbi12d 335 . . . . 5 (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
109imbi2d 331 . . . 4 (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴))))
11 eleq1 2832 . . . . . 6 (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) ↔ 𝐶 ∈ suc (card‘( 𝐴𝐵))))
12 fveq2 6377 . . . . . . 7 (𝑦 = 𝐶 → (𝐺𝑦) = (𝐺𝐶))
1312eleq1d 2829 . . . . . 6 (𝑦 = 𝐶 → ((𝐺𝑦) ∈ 𝐴 ↔ (𝐺𝐶) ∈ 𝐴))
1411, 13imbi12d 335 . . . . 5 (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝐶) ∈ 𝐴)))
1514imbi2d 331 . . . 4 (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝐶) ∈ 𝐴))))
16 r19.21v 3107 . . . . . 6 (∀𝑎𝑦 (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
172onordi 6014 . . . . . . . . . . . . . . 15 Ord suc (card‘( 𝐴𝐵))
1817a1i 11 . . . . . . . . . . . . . 14 (𝜑 → Ord suc (card‘( 𝐴𝐵)))
19 ordelss 5926 . . . . . . . . . . . . . 14 ((Ord suc (card‘( 𝐴𝐵)) ∧ 𝑦 ∈ suc (card‘( 𝐴𝐵))) → 𝑦 ⊆ suc (card‘( 𝐴𝐵)))
2018, 19sylan 575 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → 𝑦 ⊆ suc (card‘( 𝐴𝐵)))
2120sselda 3763 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) ∧ 𝑎𝑦) → 𝑎 ∈ suc (card‘( 𝐴𝐵)))
22 biimt 351 . . . . . . . . . . . 12 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → ((𝐺𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
2321, 22syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) ∧ 𝑎𝑦) → ((𝐺𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
2423ralbidva 3132 . . . . . . . . . 10 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → (∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴 ↔ ∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
252onssi 7237 . . . . . . . . . . . . . 14 suc (card‘( 𝐴𝐵)) ⊆ On
26 simprl 787 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘( 𝐴𝐵)))
2725, 26sseldi 3761 . . . . . . . . . . . . 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 9588 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ On) → (𝐺𝑦) = if(𝑦 = 𝑦, if(𝑦 = ∅, 𝐵, (𝐺𝑦)), ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅))))
3327, 32syldan 585 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → (𝐺𝑦) = if(𝑦 = 𝑦, if(𝑦 = ∅, 𝐵, (𝐺𝑦)), ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅))))
3429ad3antrrr 721 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑦 = ∅) → 𝐵𝐴)
35 inss2 3995 . . . . . . . . . . . . . . . . . . . . 21 (𝒫 (𝐺𝑦) ∩ Fin) ⊆ Fin
36 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin))
3735, 36sseldi 3761 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
38 inss1 3994 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝒫 (𝐺𝑦)
3938, 36sseldi 3761 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 ∈ 𝒫 (𝐺𝑦))
4039elpwid 4329 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 (𝐺𝑦))
4131tfr1 7699 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 Fn On
42 fnfun 6168 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn On → Fun 𝐺)
43 funiunfv 6700 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐺 𝑣𝑦 (𝐺𝑣) = (𝐺𝑦))
4441, 42, 43mp2b 10 . . . . . . . . . . . . . . . . . . . . . 22 𝑣𝑦 (𝐺𝑣) = (𝐺𝑦)
4540, 44syl6sseqr 3814 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 𝑣𝑦 (𝐺𝑣))
46 dfss3 3752 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 𝑣𝑦 (𝐺𝑣) ↔ ∀𝑢𝑤 𝑢 𝑣𝑦 (𝐺𝑣))
47 eliun 4682 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 𝑣𝑦 (𝐺𝑣) ↔ ∃𝑣𝑦 𝑢 ∈ (𝐺𝑣))
4847ralbii 3127 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑢𝑤 𝑢 𝑣𝑦 (𝐺𝑣) ↔ ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣))
4946, 48bitri 266 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 𝑣𝑦 (𝐺𝑣) ↔ ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣))
5045, 49sylib 209 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣))
51 fveq2 6377 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (𝑓𝑢) → (𝐺𝑣) = (𝐺‘(𝑓𝑢)))
5251eleq2d 2830 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (𝑓𝑢) → (𝑢 ∈ (𝐺𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓𝑢))))
5352ac6sfi 8413 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 ∈ Fin ∧ ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣)) → ∃𝑓(𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))
5437, 50, 53syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ∃𝑓(𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))
55 eleq1 2832 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = ∅ → (𝑤𝐴 ↔ ∅ ∈ 𝐴))
56 simp-4l 801 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑)
57 fveq2 6377 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = ran 𝑓 → (𝐺𝑎) = (𝐺 ran 𝑓))
5857eleq1d 2829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = ran 𝑓 → ((𝐺𝑎) ∈ 𝐴 ↔ (𝐺 ran 𝑓) ∈ 𝐴))
59 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)
6059ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)
61 simprrl 799 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → 𝑓:𝑤𝑦)
6261adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤𝑦)
63 frn 6231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑤𝑦 → ran 𝑓𝑦)
6462, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓𝑦)
6527ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On)
66 onss 7190 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ On → 𝑦 ⊆ On)
6765, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On)
6864, 67sstrd 3773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ On)
6937adantrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → 𝑤 ∈ Fin)
7069adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ Fin)
71 ffn 6225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:𝑤𝑦𝑓 Fn 𝑤)
7262, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤)
73 dffn4 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 Fn 𝑤𝑓:𝑤onto→ran 𝑓)
7472, 73sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤onto→ran 𝑓)
75 fofi 8461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤 ∈ Fin ∧ 𝑓:𝑤onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7670, 74, 75syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin)
77 dm0rn0 5512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
7861fdmd 6234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → dom 𝑓 = 𝑤)
7978eqeq1d 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → (dom 𝑓 = ∅ ↔ 𝑤 = ∅))
8077, 79syl5bbr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → (ran 𝑓 = ∅ ↔ 𝑤 = ∅))
8180necon3bid 2981 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅))
8281biimpar 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅)
83 ordunifi 8419 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran 𝑓 ⊆ On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ∈ ran 𝑓)
8468, 76, 82, 83syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ ran 𝑓)
8564, 84sseldd 3764 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓𝑦)
8658, 60, 85rspcdva 3468 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → (𝐺 ran 𝑓) ∈ 𝐴)
87 simp-4l 801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝜑)
8827ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑦 ∈ On)
8988, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑦 ⊆ On)
90 ffvelrn 6549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓:𝑤𝑦𝑢𝑤) → (𝑓𝑢) ∈ 𝑦)
9190adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ∈ 𝑦)
9289, 91sseldd 3764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ∈ On)
9363ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → ran 𝑓𝑦)
9493, 89sstrd 3773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → ran 𝑓 ⊆ On)
95 vex 3353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑓 ∈ V
9695rnex 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran 𝑓 ∈ V
9796ssonunii 7187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ran 𝑓 ⊆ On → ran 𝑓 ∈ On)
9894, 97syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → ran 𝑓 ∈ On)
9971ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑓 Fn 𝑤)
100 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑢𝑤)
101 fnfvelrn 6548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 Fn 𝑤𝑢𝑤) → (𝑓𝑢) ∈ ran 𝑓)
10299, 100, 101syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ∈ ran 𝑓)
103 elssuni 4627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓𝑢) ∈ ran 𝑓 → (𝑓𝑢) ⊆ ran 𝑓)
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ⊆ ran 𝑓)
10528, 29, 30, 31ttukeylem5 9590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ ((𝑓𝑢) ∈ On ∧ ran 𝑓 ∈ On ∧ (𝑓𝑢) ⊆ ran 𝑓)) → (𝐺‘(𝑓𝑢)) ⊆ (𝐺 ran 𝑓))
10687, 92, 98, 104, 105syl13anc 1491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝐺‘(𝑓𝑢)) ⊆ (𝐺 ran 𝑓))
107106sseld 3762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑢 ∈ (𝐺‘(𝑓𝑢)) → 𝑢 ∈ (𝐺 ran 𝑓)))
108107anassrs 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ 𝑓:𝑤𝑦) ∧ 𝑢𝑤) → (𝑢 ∈ (𝐺‘(𝑓𝑢)) → 𝑢 ∈ (𝐺 ran 𝑓)))
109108ralimdva 3109 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ 𝑓:𝑤𝑦) → (∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢)) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓)))
110109expimpd 445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ((𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓)))
111110impr 446 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓))
112111adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓))
113 dfss3 3752 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ⊆ (𝐺 ran 𝑓) ↔ ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓))
114112, 113sylibr 225 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺 ran 𝑓))
11528, 29, 30ttukeylem2 9587 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝐺 ran 𝑓) ∈ 𝐴𝑤 ⊆ (𝐺 ran 𝑓))) → 𝑤𝐴)
11656, 86, 114, 115syl12anc 865 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤𝐴)
117 0ss 4136 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∅ ⊆ 𝐵
11828, 29, 30ttukeylem2 9587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐵𝐴 ∧ ∅ ⊆ 𝐵)) → ∅ ∈ 𝐴)
119117, 118mpanr2 695 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝐵𝐴) → ∅ ∈ 𝐴)
12029, 119mpdan 678 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∅ ∈ 𝐴)
121120ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → ∅ ∈ 𝐴)
12255, 116, 121pm2.61ne 3022 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → 𝑤𝐴)
123122expr 448 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ((𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))) → 𝑤𝐴))
124123exlimdv 2028 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → (∃𝑓(𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))) → 𝑤𝐴))
12554, 124mpd 15 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤𝐴)
126125ex 401 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) → 𝑤𝐴))
127126ssrdv 3769 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝐴)
12828, 29, 30ttukeylem1 9586 . . . . . . . . . . . . . . . . 17 (𝜑 → ( (𝐺𝑦) ∈ 𝐴 ↔ (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝐴))
129128ad2antrr 717 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → ( (𝐺𝑦) ∈ 𝐴 ↔ (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝐴))
130127, 129mpbird 248 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → (𝐺𝑦) ∈ 𝐴)
131130adantr 472 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ ¬ 𝑦 = ∅) → (𝐺𝑦) ∈ 𝐴)
13234, 131ifclda 4279 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → if(𝑦 = ∅, 𝐵, (𝐺𝑦)) ∈ 𝐴)
133 uneq2 3925 . . . . . . . . . . . . . . 15 ({(𝐹 𝑦)} = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) = ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)))
134133eleq1d 2829 . . . . . . . . . . . . . 14 ({(𝐹 𝑦)} = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → (((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴 ↔ ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)) ∈ 𝐴))
135 un0 4131 . . . . . . . . . . . . . . . 16 ((𝐺 𝑦) ∪ ∅) = (𝐺 𝑦)
136 uneq2 3925 . . . . . . . . . . . . . . . 16 (∅ = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → ((𝐺 𝑦) ∪ ∅) = ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)))
137135, 136syl5eqr 2813 . . . . . . . . . . . . . . 15 (∅ = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → (𝐺 𝑦) = ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)))
138137eleq1d 2829 . . . . . . . . . . . . . 14 (∅ = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → ((𝐺 𝑦) ∈ 𝐴 ↔ ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)) ∈ 𝐴))
139 simpr 477 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) ∧ ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴) → ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴)
140 fveq2 6377 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑦 → (𝐺𝑎) = (𝐺 𝑦))
141140eleq1d 2829 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑦 → ((𝐺𝑎) ∈ 𝐴 ↔ (𝐺 𝑦) ∈ 𝐴))
142 simplrr 796 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)
143 vuniex 7154 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
144143sucid 5989 . . . . . . . . . . . . . . . . 17 𝑦 ∈ suc 𝑦
145 eloni 5920 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On → Ord 𝑦)
146 orduniorsuc 7230 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 → (𝑦 = 𝑦𝑦 = suc 𝑦))
14727, 145, 1463syl 18 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → (𝑦 = 𝑦𝑦 = suc 𝑦))
148147orcanai 1025 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → 𝑦 = suc 𝑦)
149144, 148syl5eleqr 2851 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → 𝑦𝑦)
150141, 142, 149rspcdva 3468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → (𝐺 𝑦) ∈ 𝐴)
151150adantr 472 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) ∧ ¬ ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴) → (𝐺 𝑦) ∈ 𝐴)
152134, 138, 139, 151ifbothda 4282 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)) ∈ 𝐴)
153132, 152ifclda 4279 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → if(𝑦 = 𝑦, if(𝑦 = ∅, 𝐵, (𝐺𝑦)), ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅))) ∈ 𝐴)
15433, 153eqeltrd 2844 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → (𝐺𝑦) ∈ 𝐴)
155154expr 448 . . . . . . . . . 10 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → (∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴 → (𝐺𝑦) ∈ 𝐴))
15624, 155sylbird 251 . . . . . . . . 9 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → (∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴))
157156ex 401 . . . . . . . 8 (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴)))
158157com23 86 . . . . . . 7 (𝜑 → (∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴) → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)))
159158a2i 14 . . . . . 6 ((𝜑 → ∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)))
16016, 159sylbi 208 . . . . 5 (∀𝑎𝑦 (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)))
161160a1i 11 . . . 4 (𝑦 ∈ On → (∀𝑎𝑦 (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴))))
16210, 15, 161tfis3 7257 . . 3 (𝐶 ∈ On → (𝜑 → (𝐶 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝐶) ∈ 𝐴)))
163162impd 398 . 2 (𝐶 ∈ On → ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → (𝐺𝐶) ∈ 𝐴))
1645, 163mpcom 38 1 ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → (𝐺𝐶) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  wal 1650   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  Vcvv 3350  cdif 3731  cun 3732  cin 3733  wss 3734  c0 4081  ifcif 4245  𝒫 cpw 4317  {csn 4336   cuni 4596   ciun 4678  cmpt 4890  dom cdm 5279  ran crn 5280  cima 5282  Ord word 5909  Oncon0 5910  suc csuc 5912  Fun wfun 6064   Fn wfn 6065  wf 6066  ontowfo 6068  1-1-ontowf1o 6069  cfv 6070  recscrecs 7673  Fincfn 8162  cardccrd 9014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-om 7266  df-wrecs 7612  df-recs 7674  df-1o 7766  df-er 7949  df-en 8163  df-dom 8164  df-fin 8166  df-card 9018
This theorem is referenced by:  ttukeylem7  9592
  Copyright terms: Public domain W3C validator