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

Theorem ttukey2g 10513
Description: The TeichmΓΌller-Tukey Lemma ttukey 10515 with a slightly stronger conclusion: we can set up the maximal element of 𝐴 so that it also contains some given 𝐡 ∈ 𝐴 as a subset. (Contributed by Mario Carneiro, 15-May-2015.)
Assertion
Ref Expression
ttukey2g ((βˆͺ 𝐴 ∈ dom card ∧ 𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ βˆƒπ‘₯ ∈ 𝐴 (𝐡 βŠ† π‘₯ ∧ βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ ⊊ 𝑦))
Distinct variable groups:   π‘₯,𝑦,𝐴   π‘₯,𝐡,𝑦

Proof of Theorem ttukey2g
Dummy variables 𝑀 𝑓 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 difss 4130 . . . 4 (βˆͺ 𝐴 βˆ– 𝐡) βŠ† βˆͺ 𝐴
2 ssnum 10036 . . . 4 ((βˆͺ 𝐴 ∈ dom card ∧ (βˆͺ 𝐴 βˆ– 𝐡) βŠ† βˆͺ 𝐴) β†’ (βˆͺ 𝐴 βˆ– 𝐡) ∈ dom card)
31, 2mpan2 687 . . 3 (βˆͺ 𝐴 ∈ dom card β†’ (βˆͺ 𝐴 βˆ– 𝐡) ∈ dom card)
4 isnum3 9951 . . . . 5 ((βˆͺ 𝐴 βˆ– 𝐡) ∈ dom card ↔ (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β‰ˆ (βˆͺ 𝐴 βˆ– 𝐡))
5 bren 8951 . . . . 5 ((cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β‰ˆ (βˆͺ 𝐴 βˆ– 𝐡) ↔ βˆƒπ‘“ 𝑓:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡))
64, 5bitri 274 . . . 4 ((βˆͺ 𝐴 βˆ– 𝐡) ∈ dom card ↔ βˆƒπ‘“ 𝑓:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡))
7 simp1 1134 . . . . . . 7 ((𝑓:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡) ∧ 𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ 𝑓:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡))
8 simp2 1135 . . . . . . 7 ((𝑓:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡) ∧ 𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ 𝐡 ∈ 𝐴)
9 simp3 1136 . . . . . . 7 ((𝑓:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡) ∧ 𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴))
10 dmeq 5902 . . . . . . . . . . 11 (𝑀 = 𝑧 β†’ dom 𝑀 = dom 𝑧)
1110unieqd 4921 . . . . . . . . . . 11 (𝑀 = 𝑧 β†’ βˆͺ dom 𝑀 = βˆͺ dom 𝑧)
1210, 11eqeq12d 2746 . . . . . . . . . 10 (𝑀 = 𝑧 β†’ (dom 𝑀 = βˆͺ dom 𝑀 ↔ dom 𝑧 = βˆͺ dom 𝑧))
1310eqeq1d 2732 . . . . . . . . . . 11 (𝑀 = 𝑧 β†’ (dom 𝑀 = βˆ… ↔ dom 𝑧 = βˆ…))
14 rneq 5934 . . . . . . . . . . . 12 (𝑀 = 𝑧 β†’ ran 𝑀 = ran 𝑧)
1514unieqd 4921 . . . . . . . . . . 11 (𝑀 = 𝑧 β†’ βˆͺ ran 𝑀 = βˆͺ ran 𝑧)
1613, 15ifbieq2d 4553 . . . . . . . . . 10 (𝑀 = 𝑧 β†’ if(dom 𝑀 = βˆ…, 𝐡, βˆͺ ran 𝑀) = if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧))
17 id 22 . . . . . . . . . . . 12 (𝑀 = 𝑧 β†’ 𝑀 = 𝑧)
1817, 11fveq12d 6897 . . . . . . . . . . 11 (𝑀 = 𝑧 β†’ (π‘€β€˜βˆͺ dom 𝑀) = (π‘§β€˜βˆͺ dom 𝑧))
1911fveq2d 6894 . . . . . . . . . . . . . . 15 (𝑀 = 𝑧 β†’ (π‘“β€˜βˆͺ dom 𝑀) = (π‘“β€˜βˆͺ dom 𝑧))
2019sneqd 4639 . . . . . . . . . . . . . 14 (𝑀 = 𝑧 β†’ {(π‘“β€˜βˆͺ dom 𝑀)} = {(π‘“β€˜βˆͺ dom 𝑧)})
2118, 20uneq12d 4163 . . . . . . . . . . . . 13 (𝑀 = 𝑧 β†’ ((π‘€β€˜βˆͺ dom 𝑀) βˆͺ {(π‘“β€˜βˆͺ dom 𝑀)}) = ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(π‘“β€˜βˆͺ dom 𝑧)}))
2221eleq1d 2816 . . . . . . . . . . . 12 (𝑀 = 𝑧 β†’ (((π‘€β€˜βˆͺ dom 𝑀) βˆͺ {(π‘“β€˜βˆͺ dom 𝑀)}) ∈ 𝐴 ↔ ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(π‘“β€˜βˆͺ dom 𝑧)}) ∈ 𝐴))
2322, 20ifbieq1d 4551 . . . . . . . . . . 11 (𝑀 = 𝑧 β†’ if(((π‘€β€˜βˆͺ dom 𝑀) βˆͺ {(π‘“β€˜βˆͺ dom 𝑀)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑀)}, βˆ…) = if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(π‘“β€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑧)}, βˆ…))
2418, 23uneq12d 4163 . . . . . . . . . 10 (𝑀 = 𝑧 β†’ ((π‘€β€˜βˆͺ dom 𝑀) βˆͺ if(((π‘€β€˜βˆͺ dom 𝑀) βˆͺ {(π‘“β€˜βˆͺ dom 𝑀)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑀)}, βˆ…)) = ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(π‘“β€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑧)}, βˆ…)))
2512, 16, 24ifbieq12d 4555 . . . . . . . . 9 (𝑀 = 𝑧 β†’ if(dom 𝑀 = βˆͺ dom 𝑀, if(dom 𝑀 = βˆ…, 𝐡, βˆͺ ran 𝑀), ((π‘€β€˜βˆͺ dom 𝑀) βˆͺ if(((π‘€β€˜βˆͺ dom 𝑀) βˆͺ {(π‘“β€˜βˆͺ dom 𝑀)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑀)}, βˆ…))) = if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(π‘“β€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑧)}, βˆ…))))
2625cbvmptv 5260 . . . . . . . 8 (𝑀 ∈ V ↦ if(dom 𝑀 = βˆͺ dom 𝑀, if(dom 𝑀 = βˆ…, 𝐡, βˆͺ ran 𝑀), ((π‘€β€˜βˆͺ dom 𝑀) βˆͺ if(((π‘€β€˜βˆͺ dom 𝑀) βˆͺ {(π‘“β€˜βˆͺ dom 𝑀)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑀)}, βˆ…)))) = (𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(π‘“β€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑧)}, βˆ…))))
27 recseq 8376 . . . . . . . 8 ((𝑀 ∈ V ↦ if(dom 𝑀 = βˆͺ dom 𝑀, if(dom 𝑀 = βˆ…, 𝐡, βˆͺ ran 𝑀), ((π‘€β€˜βˆͺ dom 𝑀) βˆͺ if(((π‘€β€˜βˆͺ dom 𝑀) βˆͺ {(π‘“β€˜βˆͺ dom 𝑀)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑀)}, βˆ…)))) = (𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(π‘“β€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑧)}, βˆ…)))) β†’ recs((𝑀 ∈ V ↦ if(dom 𝑀 = βˆͺ dom 𝑀, if(dom 𝑀 = βˆ…, 𝐡, βˆͺ ran 𝑀), ((π‘€β€˜βˆͺ dom 𝑀) βˆͺ if(((π‘€β€˜βˆͺ dom 𝑀) βˆͺ {(π‘“β€˜βˆͺ dom 𝑀)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑀)}, βˆ…))))) = recs((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(π‘“β€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑧)}, βˆ…))))))
2826, 27ax-mp 5 . . . . . . 7 recs((𝑀 ∈ V ↦ if(dom 𝑀 = βˆͺ dom 𝑀, if(dom 𝑀 = βˆ…, 𝐡, βˆͺ ran 𝑀), ((π‘€β€˜βˆͺ dom 𝑀) βˆͺ if(((π‘€β€˜βˆͺ dom 𝑀) βˆͺ {(π‘“β€˜βˆͺ dom 𝑀)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑀)}, βˆ…))))) = recs((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(π‘“β€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(π‘“β€˜βˆͺ dom 𝑧)}, βˆ…)))))
297, 8, 9, 28ttukeylem7 10512 . . . . . 6 ((𝑓:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡) ∧ 𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ βˆƒπ‘₯ ∈ 𝐴 (𝐡 βŠ† π‘₯ ∧ βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ ⊊ 𝑦))
30293expib 1120 . . . . 5 (𝑓:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡) β†’ ((𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ βˆƒπ‘₯ ∈ 𝐴 (𝐡 βŠ† π‘₯ ∧ βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ ⊊ 𝑦)))
3130exlimiv 1931 . . . 4 (βˆƒπ‘“ 𝑓:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡) β†’ ((𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ βˆƒπ‘₯ ∈ 𝐴 (𝐡 βŠ† π‘₯ ∧ βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ ⊊ 𝑦)))
326, 31sylbi 216 . . 3 ((βˆͺ 𝐴 βˆ– 𝐡) ∈ dom card β†’ ((𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ βˆƒπ‘₯ ∈ 𝐴 (𝐡 βŠ† π‘₯ ∧ βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ ⊊ 𝑦)))
333, 32syl 17 . 2 (βˆͺ 𝐴 ∈ dom card β†’ ((𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ βˆƒπ‘₯ ∈ 𝐴 (𝐡 βŠ† π‘₯ ∧ βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ ⊊ 𝑦)))
34333impib 1114 1 ((βˆͺ 𝐴 ∈ dom card ∧ 𝐡 ∈ 𝐴 ∧ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴)) β†’ βˆƒπ‘₯ ∈ 𝐴 (𝐡 βŠ† π‘₯ ∧ βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ ⊊ 𝑦))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085  βˆ€wal 1537   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104  βˆ€wral 3059  βˆƒwrex 3068  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947   ⊊ wpss 3948  βˆ…c0 4321  ifcif 4527  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907   class class class wbr 5147   ↦ cmpt 5230  dom cdm 5675  ran crn 5676  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542  recscrecs 8372   β‰ˆ cen 8938  Fincfn 8941  cardccrd 9932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-fin 8945  df-card 9936
This theorem is referenced by:  ttukeyg  10514
  Copyright terms: Public domain W3C validator