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

Theorem ttukeylem7 10556
Description: Lemma for ttukey 10559. (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
ttukeylem7 (𝜑 → ∃𝑥𝐴 (𝐵𝑥 ∧ ∀𝑦𝐴 ¬ 𝑥𝑦))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐺   𝜑,𝑦,𝑧   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧   𝑥,𝐹,𝑧
Allowed substitution hints:   𝜑(𝑥)   𝐹(𝑦)

Proof of Theorem ttukeylem7
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 fvex 6918 . . . 4 (card‘( 𝐴𝐵)) ∈ V
21sucid 6465 . . 3 (card‘( 𝐴𝐵)) ∈ suc (card‘( 𝐴𝐵))
3 ttukeylem.1 . . . 4 (𝜑𝐹:(card‘( 𝐴𝐵))–1-1-onto→( 𝐴𝐵))
4 ttukeylem.2 . . . 4 (𝜑𝐵𝐴)
5 ttukeylem.3 . . . 4 (𝜑 → ∀𝑥(𝑥𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴))
6 ttukeylem.4 . . . 4 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅)))))
73, 4, 5, 6ttukeylem6 10555 . . 3 ((𝜑 ∧ (card‘( 𝐴𝐵)) ∈ suc (card‘( 𝐴𝐵))) → (𝐺‘(card‘( 𝐴𝐵))) ∈ 𝐴)
82, 7mpan2 691 . 2 (𝜑 → (𝐺‘(card‘( 𝐴𝐵))) ∈ 𝐴)
93, 4, 5, 6ttukeylem4 10553 . . 3 (𝜑 → (𝐺‘∅) = 𝐵)
10 0elon 6437 . . . . 5 ∅ ∈ On
11 cardon 9985 . . . . 5 (card‘( 𝐴𝐵)) ∈ On
12 0ss 4399 . . . . 5 ∅ ⊆ (card‘( 𝐴𝐵))
1310, 11, 123pm3.2i 1339 . . . 4 (∅ ∈ On ∧ (card‘( 𝐴𝐵)) ∈ On ∧ ∅ ⊆ (card‘( 𝐴𝐵)))
143, 4, 5, 6ttukeylem5 10554 . . . 4 ((𝜑 ∧ (∅ ∈ On ∧ (card‘( 𝐴𝐵)) ∈ On ∧ ∅ ⊆ (card‘( 𝐴𝐵)))) → (𝐺‘∅) ⊆ (𝐺‘(card‘( 𝐴𝐵))))
1513, 14mpan2 691 . . 3 (𝜑 → (𝐺‘∅) ⊆ (𝐺‘(card‘( 𝐴𝐵))))
169, 15eqsstrrd 4018 . 2 (𝜑𝐵 ⊆ (𝐺‘(card‘( 𝐴𝐵))))
17 simprr 772 . . . . . 6 ((𝜑 ∧ (𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦)) → (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦)
18 ssun1 4177 . . . . . . . 8 𝑦 ⊆ (𝑦𝐵)
19 undif1 4475 . . . . . . . 8 ((𝑦𝐵) ∪ 𝐵) = (𝑦𝐵)
2018, 19sseqtrri 4032 . . . . . . 7 𝑦 ⊆ ((𝑦𝐵) ∪ 𝐵)
21 simpl 482 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝜑)
22 f1ocnv 6859 . . . . . . . . . . . . . . . . 17 (𝐹:(card‘( 𝐴𝐵))–1-1-onto→( 𝐴𝐵) → 𝐹:( 𝐴𝐵)–1-1-onto→(card‘( 𝐴𝐵)))
23 f1of 6847 . . . . . . . . . . . . . . . . 17 (𝐹:( 𝐴𝐵)–1-1-onto→(card‘( 𝐴𝐵)) → 𝐹:( 𝐴𝐵)⟶(card‘( 𝐴𝐵)))
243, 22, 233syl 18 . . . . . . . . . . . . . . . 16 (𝜑𝐹:( 𝐴𝐵)⟶(card‘( 𝐴𝐵)))
2524adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝐹:( 𝐴𝐵)⟶(card‘( 𝐴𝐵)))
26 eldifi 4130 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ (𝑦𝐵) → 𝑎𝑦)
2726ad2antll 729 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑎𝑦)
28 simprll 778 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑦𝐴)
29 elunii 4911 . . . . . . . . . . . . . . . . 17 ((𝑎𝑦𝑦𝐴) → 𝑎 𝐴)
3027, 28, 29syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑎 𝐴)
31 eldifn 4131 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝑦𝐵) → ¬ 𝑎𝐵)
3231ad2antll 729 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → ¬ 𝑎𝐵)
3330, 32eldifd 3961 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑎 ∈ ( 𝐴𝐵))
3425, 33ffvelcdmd 7104 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐹𝑎) ∈ (card‘( 𝐴𝐵)))
35 onelon 6408 . . . . . . . . . . . . . 14 (((card‘( 𝐴𝐵)) ∈ On ∧ (𝐹𝑎) ∈ (card‘( 𝐴𝐵))) → (𝐹𝑎) ∈ On)
3611, 34, 35sylancr 587 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐹𝑎) ∈ On)
37 onsuc 7832 . . . . . . . . . . . . 13 ((𝐹𝑎) ∈ On → suc (𝐹𝑎) ∈ On)
3836, 37syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → suc (𝐹𝑎) ∈ On)
3911a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (card‘( 𝐴𝐵)) ∈ On)
4011onordi 6494 . . . . . . . . . . . . 13 Ord (card‘( 𝐴𝐵))
41 ordsucss 7839 . . . . . . . . . . . . 13 (Ord (card‘( 𝐴𝐵)) → ((𝐹𝑎) ∈ (card‘( 𝐴𝐵)) → suc (𝐹𝑎) ⊆ (card‘( 𝐴𝐵))))
4240, 34, 41mpsyl 68 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → suc (𝐹𝑎) ⊆ (card‘( 𝐴𝐵)))
433, 4, 5, 6ttukeylem5 10554 . . . . . . . . . . . 12 ((𝜑 ∧ (suc (𝐹𝑎) ∈ On ∧ (card‘( 𝐴𝐵)) ∈ On ∧ suc (𝐹𝑎) ⊆ (card‘( 𝐴𝐵)))) → (𝐺‘suc (𝐹𝑎)) ⊆ (𝐺‘(card‘( 𝐴𝐵))))
4421, 38, 39, 42, 43syl13anc 1373 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐺‘suc (𝐹𝑎)) ⊆ (𝐺‘(card‘( 𝐴𝐵))))
45 ssun2 4178 . . . . . . . . . . . . 13 if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅) ⊆ ((𝐺 suc (𝐹𝑎)) ∪ if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅))
46 eloni 6393 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑎) ∈ On → Ord (𝐹𝑎))
47 ordunisuc 7853 . . . . . . . . . . . . . . . . . 18 (Ord (𝐹𝑎) → suc (𝐹𝑎) = (𝐹𝑎))
4836, 46, 473syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → suc (𝐹𝑎) = (𝐹𝑎))
4948fveq2d 6909 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐹 suc (𝐹𝑎)) = (𝐹‘(𝐹𝑎)))
503adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝐹:(card‘( 𝐴𝐵))–1-1-onto→( 𝐴𝐵))
51 f1ocnvfv2 7298 . . . . . . . . . . . . . . . . 17 ((𝐹:(card‘( 𝐴𝐵))–1-1-onto→( 𝐴𝐵) ∧ 𝑎 ∈ ( 𝐴𝐵)) → (𝐹‘(𝐹𝑎)) = 𝑎)
5250, 33, 51syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐹‘(𝐹𝑎)) = 𝑎)
5349, 52eqtr2d 2777 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑎 = (𝐹 suc (𝐹𝑎)))
54 velsn 4641 . . . . . . . . . . . . . . 15 (𝑎 ∈ {(𝐹 suc (𝐹𝑎))} ↔ 𝑎 = (𝐹 suc (𝐹𝑎)))
5553, 54sylibr 234 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑎 ∈ {(𝐹 suc (𝐹𝑎))})
5648fveq2d 6909 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐺 suc (𝐹𝑎)) = (𝐺‘(𝐹𝑎)))
57 ordelss 6399 . . . . . . . . . . . . . . . . . . . . 21 ((Ord (card‘( 𝐴𝐵)) ∧ (𝐹𝑎) ∈ (card‘( 𝐴𝐵))) → (𝐹𝑎) ⊆ (card‘( 𝐴𝐵)))
5840, 34, 57sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐹𝑎) ⊆ (card‘( 𝐴𝐵)))
593, 4, 5, 6ttukeylem5 10554 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝐹𝑎) ∈ On ∧ (card‘( 𝐴𝐵)) ∈ On ∧ (𝐹𝑎) ⊆ (card‘( 𝐴𝐵)))) → (𝐺‘(𝐹𝑎)) ⊆ (𝐺‘(card‘( 𝐴𝐵))))
6021, 36, 39, 58, 59syl13anc 1373 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐺‘(𝐹𝑎)) ⊆ (𝐺‘(card‘( 𝐴𝐵))))
6156, 60eqsstrd 4017 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐺 suc (𝐹𝑎)) ⊆ (𝐺‘(card‘( 𝐴𝐵))))
62 simprlr 779 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦)
6361, 62sstrd 3993 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐺 suc (𝐹𝑎)) ⊆ 𝑦)
6453, 27eqeltrrd 2841 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐹 suc (𝐹𝑎)) ∈ 𝑦)
6564snssd 4808 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → {(𝐹 suc (𝐹𝑎))} ⊆ 𝑦)
6663, 65unssd 4191 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → ((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ⊆ 𝑦)
673, 4, 5ttukeylem2 10551 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦𝐴 ∧ ((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ⊆ 𝑦)) → ((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴)
6821, 28, 66, 67syl12anc 836 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → ((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴)
6968iftrued 4532 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅) = {(𝐹 suc (𝐹𝑎))})
7055, 69eleqtrrd 2843 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑎 ∈ if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅))
7145, 70sselid 3980 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑎 ∈ ((𝐺 suc (𝐹𝑎)) ∪ if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅)))
723, 4, 5, 6ttukeylem3 10552 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc (𝐹𝑎) ∈ On) → (𝐺‘suc (𝐹𝑎)) = if(suc (𝐹𝑎) = suc (𝐹𝑎), if(suc (𝐹𝑎) = ∅, 𝐵, (𝐺 “ suc (𝐹𝑎))), ((𝐺 suc (𝐹𝑎)) ∪ if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅))))
7338, 72syldan 591 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐺‘suc (𝐹𝑎)) = if(suc (𝐹𝑎) = suc (𝐹𝑎), if(suc (𝐹𝑎) = ∅, 𝐵, (𝐺 “ suc (𝐹𝑎))), ((𝐺 suc (𝐹𝑎)) ∪ if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅))))
74 sucidg 6464 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑎) ∈ (card‘( 𝐴𝐵)) → (𝐹𝑎) ∈ suc (𝐹𝑎))
7534, 74syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐹𝑎) ∈ suc (𝐹𝑎))
76 ordirr 6401 . . . . . . . . . . . . . . . . . 18 (Ord (𝐹𝑎) → ¬ (𝐹𝑎) ∈ (𝐹𝑎))
7736, 46, 763syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → ¬ (𝐹𝑎) ∈ (𝐹𝑎))
78 nelne1 3038 . . . . . . . . . . . . . . . . 17 (((𝐹𝑎) ∈ suc (𝐹𝑎) ∧ ¬ (𝐹𝑎) ∈ (𝐹𝑎)) → suc (𝐹𝑎) ≠ (𝐹𝑎))
7975, 77, 78syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → suc (𝐹𝑎) ≠ (𝐹𝑎))
8079, 48neeqtrrd 3014 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → suc (𝐹𝑎) ≠ suc (𝐹𝑎))
8180neneqd 2944 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → ¬ suc (𝐹𝑎) = suc (𝐹𝑎))
8281iffalsed 4535 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → if(suc (𝐹𝑎) = suc (𝐹𝑎), if(suc (𝐹𝑎) = ∅, 𝐵, (𝐺 “ suc (𝐹𝑎))), ((𝐺 suc (𝐹𝑎)) ∪ if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅))) = ((𝐺 suc (𝐹𝑎)) ∪ if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅)))
8373, 82eqtrd 2776 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → (𝐺‘suc (𝐹𝑎)) = ((𝐺 suc (𝐹𝑎)) ∪ if(((𝐺 suc (𝐹𝑎)) ∪ {(𝐹 suc (𝐹𝑎))}) ∈ 𝐴, {(𝐹 suc (𝐹𝑎))}, ∅)))
8471, 83eleqtrrd 2843 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑎 ∈ (𝐺‘suc (𝐹𝑎)))
8544, 84sseldd 3983 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦𝐵))) → 𝑎 ∈ (𝐺‘(card‘( 𝐴𝐵))))
8685expr 456 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦)) → (𝑎 ∈ (𝑦𝐵) → 𝑎 ∈ (𝐺‘(card‘( 𝐴𝐵)))))
8786ssrdv 3988 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦)) → (𝑦𝐵) ⊆ (𝐺‘(card‘( 𝐴𝐵))))
8816adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦)) → 𝐵 ⊆ (𝐺‘(card‘( 𝐴𝐵))))
8987, 88unssd 4191 . . . . . . 7 ((𝜑 ∧ (𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦)) → ((𝑦𝐵) ∪ 𝐵) ⊆ (𝐺‘(card‘( 𝐴𝐵))))
9020, 89sstrid 3994 . . . . . 6 ((𝜑 ∧ (𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦)) → 𝑦 ⊆ (𝐺‘(card‘( 𝐴𝐵))))
9117, 90eqssd 4000 . . . . 5 ((𝜑 ∧ (𝑦𝐴 ∧ (𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦)) → (𝐺‘(card‘( 𝐴𝐵))) = 𝑦)
9291expr 456 . . . 4 ((𝜑𝑦𝐴) → ((𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦 → (𝐺‘(card‘( 𝐴𝐵))) = 𝑦))
93 npss 4112 . . . 4 (¬ (𝐺‘(card‘( 𝐴𝐵))) ⊊ 𝑦 ↔ ((𝐺‘(card‘( 𝐴𝐵))) ⊆ 𝑦 → (𝐺‘(card‘( 𝐴𝐵))) = 𝑦))
9492, 93sylibr 234 . . 3 ((𝜑𝑦𝐴) → ¬ (𝐺‘(card‘( 𝐴𝐵))) ⊊ 𝑦)
9594ralrimiva 3145 . 2 (𝜑 → ∀𝑦𝐴 ¬ (𝐺‘(card‘( 𝐴𝐵))) ⊊ 𝑦)
96 sseq2 4009 . . . 4 (𝑥 = (𝐺‘(card‘( 𝐴𝐵))) → (𝐵𝑥𝐵 ⊆ (𝐺‘(card‘( 𝐴𝐵)))))
97 psseq1 4089 . . . . . 6 (𝑥 = (𝐺‘(card‘( 𝐴𝐵))) → (𝑥𝑦 ↔ (𝐺‘(card‘( 𝐴𝐵))) ⊊ 𝑦))
9897notbid 318 . . . . 5 (𝑥 = (𝐺‘(card‘( 𝐴𝐵))) → (¬ 𝑥𝑦 ↔ ¬ (𝐺‘(card‘( 𝐴𝐵))) ⊊ 𝑦))
9998ralbidv 3177 . . . 4 (𝑥 = (𝐺‘(card‘( 𝐴𝐵))) → (∀𝑦𝐴 ¬ 𝑥𝑦 ↔ ∀𝑦𝐴 ¬ (𝐺‘(card‘( 𝐴𝐵))) ⊊ 𝑦))
10096, 99anbi12d 632 . . 3 (𝑥 = (𝐺‘(card‘( 𝐴𝐵))) → ((𝐵𝑥 ∧ ∀𝑦𝐴 ¬ 𝑥𝑦) ↔ (𝐵 ⊆ (𝐺‘(card‘( 𝐴𝐵))) ∧ ∀𝑦𝐴 ¬ (𝐺‘(card‘( 𝐴𝐵))) ⊊ 𝑦)))
101100rspcev 3621 . 2 (((𝐺‘(card‘( 𝐴𝐵))) ∈ 𝐴 ∧ (𝐵 ⊆ (𝐺‘(card‘( 𝐴𝐵))) ∧ ∀𝑦𝐴 ¬ (𝐺‘(card‘( 𝐴𝐵))) ⊊ 𝑦)) → ∃𝑥𝐴 (𝐵𝑥 ∧ ∀𝑦𝐴 ¬ 𝑥𝑦))
1028, 16, 95, 101syl12anc 836 1 (𝜑 → ∃𝑥𝐴 (𝐵𝑥 ∧ ∀𝑦𝐴 ¬ 𝑥𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086  wal 1537   = wceq 1539  wcel 2107  wne 2939  wral 3060  wrex 3069  Vcvv 3479  cdif 3947  cun 3948  cin 3949  wss 3950  wpss 3951  c0 4332  ifcif 4524  𝒫 cpw 4599  {csn 4625   cuni 4906  cmpt 5224  ccnv 5683  dom cdm 5684  ran crn 5685  cima 5687  Ord word 6382  Oncon0 6383  suc csuc 6385  wf 6556  1-1-ontowf1o 6559  cfv 6560  recscrecs 8411  Fincfn 8986  cardccrd 9976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-om 7889  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-1o 8507  df-en 8987  df-dom 8988  df-fin 8990  df-card 9980
This theorem is referenced by:  ttukey2g  10557
  Copyright terms: Public domain W3C validator