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

Theorem ttukeylem6 9281
Description: Lemma for ttukey 9285. (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 8715 . . . . 5 (card‘( 𝐴𝐵)) ∈ On
21onsuci 6986 . . . 4 suc (card‘( 𝐴𝐵)) ∈ On
32a1i 11 . . 3 (𝜑 → suc (card‘( 𝐴𝐵)) ∈ On)
4 onelon 5710 . . 3 ((suc (card‘( 𝐴𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘( 𝐴𝐵))) → 𝐶 ∈ On)
53, 4sylan 488 . 2 ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → 𝐶 ∈ On)
6 eleq1 2692 . . . . . 6 (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) ↔ 𝑎 ∈ suc (card‘( 𝐴𝐵))))
7 fveq2 6150 . . . . . . 7 (𝑦 = 𝑎 → (𝐺𝑦) = (𝐺𝑎))
87eleq1d 2688 . . . . . 6 (𝑦 = 𝑎 → ((𝐺𝑦) ∈ 𝐴 ↔ (𝐺𝑎) ∈ 𝐴))
96, 8imbi12d 334 . . . . 5 (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
109imbi2d 330 . . . 4 (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴))))
11 eleq1 2692 . . . . . 6 (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) ↔ 𝐶 ∈ suc (card‘( 𝐴𝐵))))
12 fveq2 6150 . . . . . . 7 (𝑦 = 𝐶 → (𝐺𝑦) = (𝐺𝐶))
1312eleq1d 2688 . . . . . 6 (𝑦 = 𝐶 → ((𝐺𝑦) ∈ 𝐴 ↔ (𝐺𝐶) ∈ 𝐴))
1411, 13imbi12d 334 . . . . 5 (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝐶) ∈ 𝐴)))
1514imbi2d 330 . . . 4 (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝐶) ∈ 𝐴))))
16 r19.21v 2959 . . . . . 6 (∀𝑎𝑦 (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
172onordi 5794 . . . . . . . . . . . . . . 15 Ord suc (card‘( 𝐴𝐵))
1817a1i 11 . . . . . . . . . . . . . 14 (𝜑 → Ord suc (card‘( 𝐴𝐵)))
19 ordelss 5701 . . . . . . . . . . . . . 14 ((Ord suc (card‘( 𝐴𝐵)) ∧ 𝑦 ∈ suc (card‘( 𝐴𝐵))) → 𝑦 ⊆ suc (card‘( 𝐴𝐵)))
2018, 19sylan 488 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → 𝑦 ⊆ suc (card‘( 𝐴𝐵)))
2120sselda 3588 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) ∧ 𝑎𝑦) → 𝑎 ∈ suc (card‘( 𝐴𝐵)))
22 biimt 350 . . . . . . . . . . . 12 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → ((𝐺𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
2321, 22syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) ∧ 𝑎𝑦) → ((𝐺𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
2423ralbidva 2984 . . . . . . . . . 10 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → (∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴 ↔ ∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)))
252onssi 6985 . . . . . . . . . . . . . 14 suc (card‘( 𝐴𝐵)) ⊆ On
26 simprl 793 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘( 𝐴𝐵)))
2725, 26sseldi 3586 . . . . . . . . . . . . 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 9278 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ On) → (𝐺𝑦) = if(𝑦 = 𝑦, if(𝑦 = ∅, 𝐵, (𝐺𝑦)), ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅))))
3327, 32syldan 487 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → (𝐺𝑦) = if(𝑦 = 𝑦, if(𝑦 = ∅, 𝐵, (𝐺𝑦)), ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅))))
3429ad3antrrr 765 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑦 = ∅) → 𝐵𝐴)
35 inss2 3817 . . . . . . . . . . . . . . . . . . . . 21 (𝒫 (𝐺𝑦) ∩ Fin) ⊆ Fin
36 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin))
3735, 36sseldi 3586 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
38 inss1 3816 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝒫 (𝐺𝑦)
3938, 36sseldi 3586 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 ∈ 𝒫 (𝐺𝑦))
4039elpwid 4146 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 (𝐺𝑦))
4131tfr1 7439 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 Fn On
42 fnfun 5948 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn On → Fun 𝐺)
43 funiunfv 6461 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐺 𝑣𝑦 (𝐺𝑣) = (𝐺𝑦))
4441, 42, 43mp2b 10 . . . . . . . . . . . . . . . . . . . . . 22 𝑣𝑦 (𝐺𝑣) = (𝐺𝑦)
4540, 44syl6sseqr 3636 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤 𝑣𝑦 (𝐺𝑣))
46 dfss3 3578 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 𝑣𝑦 (𝐺𝑣) ↔ ∀𝑢𝑤 𝑢 𝑣𝑦 (𝐺𝑣))
47 eliun 4495 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 𝑣𝑦 (𝐺𝑣) ↔ ∃𝑣𝑦 𝑢 ∈ (𝐺𝑣))
4847ralbii 2979 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑢𝑤 𝑢 𝑣𝑦 (𝐺𝑣) ↔ ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣))
4946, 48bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 𝑣𝑦 (𝐺𝑣) ↔ ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣))
5045, 49sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣))
51 fveq2 6150 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (𝑓𝑢) → (𝐺𝑣) = (𝐺‘(𝑓𝑢)))
5251eleq2d 2689 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (𝑓𝑢) → (𝑢 ∈ (𝐺𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓𝑢))))
5352ac6sfi 8149 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 ∈ Fin ∧ ∀𝑢𝑤𝑣𝑦 𝑢 ∈ (𝐺𝑣)) → ∃𝑓(𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))
5437, 50, 53syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ∃𝑓(𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))
55 eleq1 2692 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = ∅ → (𝑤𝐴 ↔ ∅ ∈ 𝐴))
56 simp-4l 805 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑)
57 simprrl 803 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → 𝑓:𝑤𝑦)
5857adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤𝑦)
59 frn 6012 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑤𝑦 → ran 𝑓𝑦)
6058, 59syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓𝑦)
6127ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On)
62 onss 6938 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ On → 𝑦 ⊆ On)
6361, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On)
6460, 63sstrd 3598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ On)
6537adantrr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → 𝑤 ∈ Fin)
6665adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ Fin)
67 ffn 6004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:𝑤𝑦𝑓 Fn 𝑤)
6858, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤)
69 dffn4 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 Fn 𝑤𝑓:𝑤onto→ran 𝑓)
7068, 69sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤onto→ran 𝑓)
71 fofi 8197 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤 ∈ Fin ∧ 𝑓:𝑤onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7266, 70, 71syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin)
73 dm0rn0 5306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
74 fdm 6010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:𝑤𝑦 → dom 𝑓 = 𝑤)
7557, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → dom 𝑓 = 𝑤)
7675eqeq1d 2628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → (dom 𝑓 = ∅ ↔ 𝑤 = ∅))
7773, 76syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → (ran 𝑓 = ∅ ↔ 𝑤 = ∅))
7877necon3bid 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅))
7978biimpar 502 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅)
80 ordunifi 8155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran 𝑓 ⊆ On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ∈ ran 𝑓)
8164, 72, 79, 80syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ ran 𝑓)
8260, 81sseldd 3589 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓𝑦)
83 simplrr 800 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)
8483ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)
85 fveq2 6150 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = ran 𝑓 → (𝐺𝑎) = (𝐺 ran 𝑓))
8685eleq1d 2688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = ran 𝑓 → ((𝐺𝑎) ∈ 𝐴 ↔ (𝐺 ran 𝑓) ∈ 𝐴))
8786rspcv 3296 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ran 𝑓𝑦 → (∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴 → (𝐺 ran 𝑓) ∈ 𝐴))
8882, 84, 87sylc 65 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → (𝐺 ran 𝑓) ∈ 𝐴)
89 simp-4l 805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝜑)
9027ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑦 ∈ On)
9190, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑦 ⊆ On)
92 ffvelrn 6314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓:𝑤𝑦𝑢𝑤) → (𝑓𝑢) ∈ 𝑦)
9392adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ∈ 𝑦)
9491, 93sseldd 3589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ∈ On)
9559ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → ran 𝑓𝑦)
9695, 91sstrd 3598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → ran 𝑓 ⊆ On)
97 vex 3194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑓 ∈ V
9897rnex 7048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran 𝑓 ∈ V
9998ssonunii 6935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ran 𝑓 ⊆ On → ran 𝑓 ∈ On)
10096, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → ran 𝑓 ∈ On)
10167ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑓 Fn 𝑤)
102 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → 𝑢𝑤)
103 fnfvelrn 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 Fn 𝑤𝑢𝑤) → (𝑓𝑢) ∈ ran 𝑓)
104101, 102, 103syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ∈ ran 𝑓)
105 elssuni 4438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓𝑢) ∈ ran 𝑓 → (𝑓𝑢) ⊆ ran 𝑓)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑓𝑢) ⊆ ran 𝑓)
10728, 29, 30, 31ttukeylem5 9280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ ((𝑓𝑢) ∈ On ∧ ran 𝑓 ∈ On ∧ (𝑓𝑢) ⊆ ran 𝑓)) → (𝐺‘(𝑓𝑢)) ⊆ (𝐺 ran 𝑓))
10889, 94, 100, 106, 107syl13anc 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝐺‘(𝑓𝑢)) ⊆ (𝐺 ran 𝑓))
109108sseld 3587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ (𝑓:𝑤𝑦𝑢𝑤)) → (𝑢 ∈ (𝐺‘(𝑓𝑢)) → 𝑢 ∈ (𝐺 ran 𝑓)))
110109anassrs 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ 𝑓:𝑤𝑦) ∧ 𝑢𝑤) → (𝑢 ∈ (𝐺‘(𝑓𝑢)) → 𝑢 ∈ (𝐺 ran 𝑓)))
111110ralimdva 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) ∧ 𝑓:𝑤𝑦) → (∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢)) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓)))
112111expimpd 628 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ((𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓)))
113112impr 648 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓))
114113adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓))
115 dfss3 3578 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ⊆ (𝐺 ran 𝑓) ↔ ∀𝑢𝑤 𝑢 ∈ (𝐺 ran 𝑓))
116114, 115sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺 ran 𝑓))
11728, 29, 30ttukeylem2 9277 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝐺 ran 𝑓) ∈ 𝐴𝑤 ⊆ (𝐺 ran 𝑓))) → 𝑤𝐴)
11856, 88, 116, 117syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤𝐴)
119 0ss 3949 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∅ ⊆ 𝐵
12028, 29, 30ttukeylem2 9277 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐵𝐴 ∧ ∅ ⊆ 𝐵)) → ∅ ∈ 𝐴)
121119, 120mpanr2 719 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝐵𝐴) → ∅ ∈ 𝐴)
12229, 121mpdan 701 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∅ ∈ 𝐴)
123122ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → ∅ ∈ 𝐴)
12455, 118, 123pm2.61ne 2881 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) ∧ (𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))))) → 𝑤𝐴)
125124expr 642 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → ((𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))) → 𝑤𝐴))
126125exlimdv 1863 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → (∃𝑓(𝑓:𝑤𝑦 ∧ ∀𝑢𝑤 𝑢 ∈ (𝐺‘(𝑓𝑢))) → 𝑤𝐴))
12754, 126mpd 15 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ 𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin)) → 𝑤𝐴)
128127ex 450 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → (𝑤 ∈ (𝒫 (𝐺𝑦) ∩ Fin) → 𝑤𝐴))
129128ssrdv 3594 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝐴)
13028, 29, 30ttukeylem1 9276 . . . . . . . . . . . . . . . . 17 (𝜑 → ( (𝐺𝑦) ∈ 𝐴 ↔ (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝐴))
131130ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → ( (𝐺𝑦) ∈ 𝐴 ↔ (𝒫 (𝐺𝑦) ∩ Fin) ⊆ 𝐴))
132129, 131mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → (𝐺𝑦) ∈ 𝐴)
133132adantr 481 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) ∧ ¬ 𝑦 = ∅) → (𝐺𝑦) ∈ 𝐴)
13434, 133ifclda 4097 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ 𝑦 = 𝑦) → if(𝑦 = ∅, 𝐵, (𝐺𝑦)) ∈ 𝐴)
135 uneq2 3744 . . . . . . . . . . . . . . 15 ({(𝐹 𝑦)} = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) = ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)))
136135eleq1d 2688 . . . . . . . . . . . . . 14 ({(𝐹 𝑦)} = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → (((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴 ↔ ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)) ∈ 𝐴))
137 un0 3944 . . . . . . . . . . . . . . . 16 ((𝐺 𝑦) ∪ ∅) = (𝐺 𝑦)
138 uneq2 3744 . . . . . . . . . . . . . . . 16 (∅ = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → ((𝐺 𝑦) ∪ ∅) = ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)))
139137, 138syl5eqr 2674 . . . . . . . . . . . . . . 15 (∅ = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → (𝐺 𝑦) = ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)))
140139eleq1d 2688 . . . . . . . . . . . . . 14 (∅ = if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅) → ((𝐺 𝑦) ∈ 𝐴 ↔ ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)) ∈ 𝐴))
141 simpr 477 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) ∧ ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴) → ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴)
142 vuniex 6908 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
143142sucid 5766 . . . . . . . . . . . . . . . . 17 𝑦 ∈ suc 𝑦
144 eloni 5695 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On → Ord 𝑦)
145 orduniorsuc 6978 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 → (𝑦 = 𝑦𝑦 = suc 𝑦))
14627, 144, 1453syl 18 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → (𝑦 = 𝑦𝑦 = suc 𝑦))
147146orcanai 951 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → 𝑦 = suc 𝑦)
148143, 147syl5eleqr 2711 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → 𝑦𝑦)
149 simplrr 800 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)
150 fveq2 6150 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑦 → (𝐺𝑎) = (𝐺 𝑦))
151150eleq1d 2688 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑦 → ((𝐺𝑎) ∈ 𝐴 ↔ (𝐺 𝑦) ∈ 𝐴))
152151rspcv 3296 . . . . . . . . . . . . . . . 16 ( 𝑦𝑦 → (∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴 → (𝐺 𝑦) ∈ 𝐴))
153148, 149, 152sylc 65 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → (𝐺 𝑦) ∈ 𝐴)
154153adantr 481 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) ∧ ¬ ((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴) → (𝐺 𝑦) ∈ 𝐴)
155136, 140, 141, 154ifbothda 4100 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑦) → ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅)) ∈ 𝐴)
156134, 155ifclda 4097 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → if(𝑦 = 𝑦, if(𝑦 = ∅, 𝐵, (𝐺𝑦)), ((𝐺 𝑦) ∪ if(((𝐺 𝑦) ∪ {(𝐹 𝑦)}) ∈ 𝐴, {(𝐹 𝑦)}, ∅))) ∈ 𝐴)
15733, 156eqeltrd 2704 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ suc (card‘( 𝐴𝐵)) ∧ ∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴)) → (𝐺𝑦) ∈ 𝐴)
158157expr 642 . . . . . . . . . 10 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → (∀𝑎𝑦 (𝐺𝑎) ∈ 𝐴 → (𝐺𝑦) ∈ 𝐴))
15924, 158sylbird 250 . . . . . . . . 9 ((𝜑𝑦 ∈ suc (card‘( 𝐴𝐵))) → (∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴))
160159ex 450 . . . . . . . 8 (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴)))
161160com23 86 . . . . . . 7 (𝜑 → (∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴) → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)))
162161a2i 14 . . . . . 6 ((𝜑 → ∀𝑎𝑦 (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)))
16316, 162sylbi 207 . . . . 5 (∀𝑎𝑦 (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴)))
164163a1i 11 . . . 4 (𝑦 ∈ On → (∀𝑎𝑦 (𝜑 → (𝑎 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝑦) ∈ 𝐴))))
16510, 15, 164tfis3 7005 . . 3 (𝐶 ∈ On → (𝜑 → (𝐶 ∈ suc (card‘( 𝐴𝐵)) → (𝐺𝐶) ∈ 𝐴)))
166165impd 447 . 2 (𝐶 ∈ On → ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → (𝐺𝐶) ∈ 𝐴))
1675, 166mpcom 38 1 ((𝜑𝐶 ∈ suc (card‘( 𝐴𝐵))) → (𝐺𝐶) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1992  wne 2796  wral 2912  wrex 2913  Vcvv 3191  cdif 3557  cun 3558  cin 3559  wss 3560  c0 3896  ifcif 4063  𝒫 cpw 4135  {csn 4153   cuni 4407   ciun 4490  cmpt 4678  dom cdm 5079  ran crn 5080  cima 5082  Ord word 5684  Oncon0 5685  suc csuc 5687  Fun wfun 5844   Fn wfn 5845  wf 5846  ontowfo 5848  1-1-ontowf1o 5849  cfv 5850  recscrecs 7413  Fincfn 7900  cardccrd 8706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-om 7014  df-wrecs 7353  df-recs 7414  df-1o 7506  df-er 7688  df-en 7901  df-dom 7902  df-fin 7904  df-card 8710
This theorem is referenced by:  ttukeylem7  9282
  Copyright terms: Public domain W3C validator