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

Theorem ackbij1lem18 10267
Description: Lemma for ackbij1 10268. (Contributed by Stefan O'Rear, 18-Nov-2014.)
Hypothesis
Ref Expression
ackbij.f 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘ 𝑦𝑥 ({𝑦} × 𝒫 𝑦)))
Assertion
Ref Expression
ackbij1lem18 (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹𝑏) = suc (𝐹𝐴))
Distinct variable groups:   𝐹,𝑏,𝑥,𝑦   𝐴,𝑏,𝑥,𝑦

Proof of Theorem ackbij1lem18
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 difss 4128 . . . 4 (𝐴 (ω ∖ 𝐴)) ⊆ 𝐴
2 ackbij.f . . . . 5 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘ 𝑦𝑥 ({𝑦} × 𝒫 𝑦)))
32ackbij1lem11 10260 . . . 4 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 (ω ∖ 𝐴)) ⊆ 𝐴) → (𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin))
41, 3mpan2 689 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin))
5 difss 4128 . . . . . . 7 (ω ∖ 𝐴) ⊆ ω
6 omsson 7875 . . . . . . 7 ω ⊆ On
75, 6sstri 3986 . . . . . 6 (ω ∖ 𝐴) ⊆ On
8 ominf 9286 . . . . . . . 8 ¬ ω ∈ Fin
9 elinel2 4194 . . . . . . . 8 (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ Fin)
10 difinf 9345 . . . . . . . 8 ((¬ ω ∈ Fin ∧ 𝐴 ∈ Fin) → ¬ (ω ∖ 𝐴) ∈ Fin)
118, 9, 10sylancr 585 . . . . . . 7 (𝐴 ∈ (𝒫 ω ∩ Fin) → ¬ (ω ∖ 𝐴) ∈ Fin)
12 0fi 9070 . . . . . . . . 9 ∅ ∈ Fin
13 eleq1 2813 . . . . . . . . 9 ((ω ∖ 𝐴) = ∅ → ((ω ∖ 𝐴) ∈ Fin ↔ ∅ ∈ Fin))
1412, 13mpbiri 257 . . . . . . . 8 ((ω ∖ 𝐴) = ∅ → (ω ∖ 𝐴) ∈ Fin)
1514necon3bi 2956 . . . . . . 7 (¬ (ω ∖ 𝐴) ∈ Fin → (ω ∖ 𝐴) ≠ ∅)
1611, 15syl 17 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ≠ ∅)
17 onint 7794 . . . . . 6 (((ω ∖ 𝐴) ⊆ On ∧ (ω ∖ 𝐴) ≠ ∅) → (ω ∖ 𝐴) ∈ (ω ∖ 𝐴))
187, 16, 17sylancr 585 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ∈ (ω ∖ 𝐴))
1918eldifad 3956 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ∈ ω)
20 ackbij1lem4 10253 . . . 4 ( (ω ∖ 𝐴) ∈ ω → { (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin))
2119, 20syl 17 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → { (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin))
22 ackbij1lem6 10255 . . 3 (((𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ { (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin)) → ((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin))
234, 21, 22syl2anc 582 . 2 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin))
2418eldifbd 3957 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → ¬ (ω ∖ 𝐴) ∈ 𝐴)
25 disjsn 4717 . . . . . 6 ((𝐴 ∩ { (ω ∖ 𝐴)}) = ∅ ↔ ¬ (ω ∖ 𝐴) ∈ 𝐴)
2624, 25sylibr 233 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐴 ∩ { (ω ∖ 𝐴)}) = ∅)
27 ssdisj 4461 . . . . 5 (((𝐴 (ω ∖ 𝐴)) ⊆ 𝐴 ∧ (𝐴 ∩ { (ω ∖ 𝐴)}) = ∅) → ((𝐴 (ω ∖ 𝐴)) ∩ { (ω ∖ 𝐴)}) = ∅)
281, 26, 27sylancr 585 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 (ω ∖ 𝐴)) ∩ { (ω ∖ 𝐴)}) = ∅)
292ackbij1lem9 10258 . . . 4 (((𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ { (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin) ∧ ((𝐴 (ω ∖ 𝐴)) ∩ { (ω ∖ 𝐴)}) = ∅) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹‘{ (ω ∖ 𝐴)})))
304, 21, 28, 29syl3anc 1368 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹‘{ (ω ∖ 𝐴)})))
312ackbij1lem14 10263 . . . . 5 ( (ω ∖ 𝐴) ∈ ω → (𝐹‘{ (ω ∖ 𝐴)}) = suc (𝐹 (ω ∖ 𝐴)))
3219, 31syl 17 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘{ (ω ∖ 𝐴)}) = suc (𝐹 (ω ∖ 𝐴)))
3332oveq2d 7435 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹‘{ (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o suc (𝐹 (ω ∖ 𝐴))))
342ackbij1lem10 10259 . . . . . . 7 𝐹:(𝒫 ω ∩ Fin)⟶ω
3534ffvelcdmi 7092 . . . . . 6 ((𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 (ω ∖ 𝐴))) ∈ ω)
364, 35syl 17 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 (ω ∖ 𝐴))) ∈ ω)
37 ackbij1lem3 10252 . . . . . . 7 ( (ω ∖ 𝐴) ∈ ω → (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin))
3819, 37syl 17 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin))
3934ffvelcdmi 7092 . . . . . 6 ( (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin) → (𝐹 (ω ∖ 𝐴)) ∈ ω)
4038, 39syl 17 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹 (ω ∖ 𝐴)) ∈ ω)
41 nnasuc 8627 . . . . 5 (((𝐹‘(𝐴 (ω ∖ 𝐴))) ∈ ω ∧ (𝐹 (ω ∖ 𝐴)) ∈ ω) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o suc (𝐹 (ω ∖ 𝐴))) = suc ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))))
4236, 40, 41syl2anc 582 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o suc (𝐹 (ω ∖ 𝐴))) = suc ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))))
43 disjdifr 4474 . . . . . . . 8 ((𝐴 (ω ∖ 𝐴)) ∩ (ω ∖ 𝐴)) = ∅
4443a1i 11 . . . . . . 7 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 (ω ∖ 𝐴)) ∩ (ω ∖ 𝐴)) = ∅)
452ackbij1lem9 10258 . . . . . . 7 (((𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin) ∧ ((𝐴 (ω ∖ 𝐴)) ∩ (ω ∖ 𝐴)) = ∅) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴))) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))))
464, 38, 44, 45syl3anc 1368 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴))) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))))
47 uncom 4150 . . . . . . . 8 ((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴)) = ( (ω ∖ 𝐴) ∪ (𝐴 (ω ∖ 𝐴)))
48 onnmin 7802 . . . . . . . . . . . . . . 15 (((ω ∖ 𝐴) ⊆ On ∧ 𝑎 ∈ (ω ∖ 𝐴)) → ¬ 𝑎 (ω ∖ 𝐴))
497, 48mpan 688 . . . . . . . . . . . . . 14 (𝑎 ∈ (ω ∖ 𝐴) → ¬ 𝑎 (ω ∖ 𝐴))
5049con2i 139 . . . . . . . . . . . . 13 (𝑎 (ω ∖ 𝐴) → ¬ 𝑎 ∈ (ω ∖ 𝐴))
5150adantl 480 . . . . . . . . . . . 12 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 (ω ∖ 𝐴)) → ¬ 𝑎 ∈ (ω ∖ 𝐴))
52 ordom 7881 . . . . . . . . . . . . . . 15 Ord ω
53 ordelss 6387 . . . . . . . . . . . . . . 15 ((Ord ω ∧ (ω ∖ 𝐴) ∈ ω) → (ω ∖ 𝐴) ⊆ ω)
5452, 19, 53sylancr 585 . . . . . . . . . . . . . 14 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ⊆ ω)
5554sselda 3976 . . . . . . . . . . . . 13 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 (ω ∖ 𝐴)) → 𝑎 ∈ ω)
56 eldif 3954 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (ω ∖ 𝐴) ↔ (𝑎 ∈ ω ∧ ¬ 𝑎𝐴))
5756simplbi2 499 . . . . . . . . . . . . . . 15 (𝑎 ∈ ω → (¬ 𝑎𝐴𝑎 ∈ (ω ∖ 𝐴)))
5857orrd 861 . . . . . . . . . . . . . 14 (𝑎 ∈ ω → (𝑎𝐴𝑎 ∈ (ω ∖ 𝐴)))
5958orcomd 869 . . . . . . . . . . . . 13 (𝑎 ∈ ω → (𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎𝐴))
6055, 59syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 (ω ∖ 𝐴)) → (𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎𝐴))
61 orel1 886 . . . . . . . . . . . 12 𝑎 ∈ (ω ∖ 𝐴) → ((𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎𝐴) → 𝑎𝐴))
6251, 60, 61sylc 65 . . . . . . . . . . 11 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 (ω ∖ 𝐴)) → 𝑎𝐴)
6362ex 411 . . . . . . . . . 10 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝑎 (ω ∖ 𝐴) → 𝑎𝐴))
6463ssrdv 3982 . . . . . . . . 9 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ⊆ 𝐴)
65 undif 4483 . . . . . . . . 9 ( (ω ∖ 𝐴) ⊆ 𝐴 ↔ ( (ω ∖ 𝐴) ∪ (𝐴 (ω ∖ 𝐴))) = 𝐴)
6664, 65sylib 217 . . . . . . . 8 (𝐴 ∈ (𝒫 ω ∩ Fin) → ( (ω ∖ 𝐴) ∪ (𝐴 (ω ∖ 𝐴))) = 𝐴)
6747, 66eqtrid 2777 . . . . . . 7 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴)) = 𝐴)
6867fveq2d 6900 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴))) = (𝐹𝐴))
6946, 68eqtr3d 2767 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))) = (𝐹𝐴))
70 suceq 6437 . . . . 5 (((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))) = (𝐹𝐴) → suc ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))) = suc (𝐹𝐴))
7169, 70syl 17 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → suc ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))) = suc (𝐹𝐴))
7242, 71eqtrd 2765 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o suc (𝐹 (ω ∖ 𝐴))) = suc (𝐹𝐴))
7330, 33, 723eqtrd 2769 . 2 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = suc (𝐹𝐴))
74 fveqeq2 6905 . . 3 (𝑏 = ((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)}) → ((𝐹𝑏) = suc (𝐹𝐴) ↔ (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = suc (𝐹𝐴)))
7574rspcev 3606 . 2 ((((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin) ∧ (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = suc (𝐹𝐴)) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹𝑏) = suc (𝐹𝐴))
7623, 73, 75syl2anc 582 1 (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹𝑏) = suc (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wo 845   = wceq 1533  wcel 2098  wne 2929  wrex 3059  cdif 3941  cun 3942  cin 3943  wss 3944  c0 4322  𝒫 cpw 4604  {csn 4630   cint 4950   ciun 4997  cmpt 5232   × cxp 5676  Ord word 6370  Oncon0 6371  suc csuc 6373  cfv 6549  (class class class)co 7419  ωcom 7871   +o coa 8484  Fincfn 8964  cardccrd 9965
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-dju 9931  df-card 9969
This theorem is referenced by:  ackbij1  10268
  Copyright terms: Public domain W3C validator