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

Theorem ackbij1lem18 9737
Description: Lemma for ackbij1 9738. (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 4022 . . . 4 (𝐴 (ω ∖ 𝐴)) ⊆ 𝐴
2 ackbij.f . . . . 5 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘ 𝑦𝑥 ({𝑦} × 𝒫 𝑦)))
32ackbij1lem11 9730 . . . 4 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 (ω ∖ 𝐴)) ⊆ 𝐴) → (𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin))
41, 3mpan2 691 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin))
5 difss 4022 . . . . . . 7 (ω ∖ 𝐴) ⊆ ω
6 omsson 7603 . . . . . . 7 ω ⊆ On
75, 6sstri 3886 . . . . . 6 (ω ∖ 𝐴) ⊆ On
8 ominf 8809 . . . . . . . 8 ¬ ω ∈ Fin
9 elinel2 4086 . . . . . . . 8 (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ Fin)
10 difinf 8862 . . . . . . . 8 ((¬ ω ∈ Fin ∧ 𝐴 ∈ Fin) → ¬ (ω ∖ 𝐴) ∈ Fin)
118, 9, 10sylancr 590 . . . . . . 7 (𝐴 ∈ (𝒫 ω ∩ Fin) → ¬ (ω ∖ 𝐴) ∈ Fin)
12 0fin 8770 . . . . . . . . 9 ∅ ∈ Fin
13 eleq1 2820 . . . . . . . . 9 ((ω ∖ 𝐴) = ∅ → ((ω ∖ 𝐴) ∈ Fin ↔ ∅ ∈ Fin))
1412, 13mpbiri 261 . . . . . . . 8 ((ω ∖ 𝐴) = ∅ → (ω ∖ 𝐴) ∈ Fin)
1514necon3bi 2960 . . . . . . 7 (¬ (ω ∖ 𝐴) ∈ Fin → (ω ∖ 𝐴) ≠ ∅)
1611, 15syl 17 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ≠ ∅)
17 onint 7529 . . . . . 6 (((ω ∖ 𝐴) ⊆ On ∧ (ω ∖ 𝐴) ≠ ∅) → (ω ∖ 𝐴) ∈ (ω ∖ 𝐴))
187, 16, 17sylancr 590 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ∈ (ω ∖ 𝐴))
1918eldifad 3855 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ∈ ω)
20 ackbij1lem4 9723 . . . 4 ( (ω ∖ 𝐴) ∈ ω → { (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin))
2119, 20syl 17 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → { (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin))
22 ackbij1lem6 9725 . . 3 (((𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ { (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin)) → ((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin))
234, 21, 22syl2anc 587 . 2 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin))
2418eldifbd 3856 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → ¬ (ω ∖ 𝐴) ∈ 𝐴)
25 disjsn 4602 . . . . . 6 ((𝐴 ∩ { (ω ∖ 𝐴)}) = ∅ ↔ ¬ (ω ∖ 𝐴) ∈ 𝐴)
2624, 25sylibr 237 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐴 ∩ { (ω ∖ 𝐴)}) = ∅)
27 ssdisj 4349 . . . . 5 (((𝐴 (ω ∖ 𝐴)) ⊆ 𝐴 ∧ (𝐴 ∩ { (ω ∖ 𝐴)}) = ∅) → ((𝐴 (ω ∖ 𝐴)) ∩ { (ω ∖ 𝐴)}) = ∅)
281, 26, 27sylancr 590 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 (ω ∖ 𝐴)) ∩ { (ω ∖ 𝐴)}) = ∅)
292ackbij1lem9 9728 . . . 4 (((𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ { (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin) ∧ ((𝐴 (ω ∖ 𝐴)) ∩ { (ω ∖ 𝐴)}) = ∅) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹‘{ (ω ∖ 𝐴)})))
304, 21, 28, 29syl3anc 1372 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹‘{ (ω ∖ 𝐴)})))
312ackbij1lem14 9733 . . . . 5 ( (ω ∖ 𝐴) ∈ ω → (𝐹‘{ (ω ∖ 𝐴)}) = suc (𝐹 (ω ∖ 𝐴)))
3219, 31syl 17 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘{ (ω ∖ 𝐴)}) = suc (𝐹 (ω ∖ 𝐴)))
3332oveq2d 7186 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹‘{ (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o suc (𝐹 (ω ∖ 𝐴))))
342ackbij1lem10 9729 . . . . . . 7 𝐹:(𝒫 ω ∩ Fin)⟶ω
3534ffvelrni 6860 . . . . . 6 ((𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 (ω ∖ 𝐴))) ∈ ω)
364, 35syl 17 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 (ω ∖ 𝐴))) ∈ ω)
37 ackbij1lem3 9722 . . . . . . 7 ( (ω ∖ 𝐴) ∈ ω → (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin))
3819, 37syl 17 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin))
3934ffvelrni 6860 . . . . . 6 ( (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin) → (𝐹 (ω ∖ 𝐴)) ∈ ω)
4038, 39syl 17 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹 (ω ∖ 𝐴)) ∈ ω)
41 nnasuc 8263 . . . . 5 (((𝐹‘(𝐴 (ω ∖ 𝐴))) ∈ ω ∧ (𝐹 (ω ∖ 𝐴)) ∈ ω) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o suc (𝐹 (ω ∖ 𝐴))) = suc ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))))
4236, 40, 41syl2anc 587 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o suc (𝐹 (ω ∖ 𝐴))) = suc ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))))
43 disjdifr 4362 . . . . . . . 8 ((𝐴 (ω ∖ 𝐴)) ∩ (ω ∖ 𝐴)) = ∅
4443a1i 11 . . . . . . 7 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 (ω ∖ 𝐴)) ∩ (ω ∖ 𝐴)) = ∅)
452ackbij1lem9 9728 . . . . . . 7 (((𝐴 (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin) ∧ ((𝐴 (ω ∖ 𝐴)) ∩ (ω ∖ 𝐴)) = ∅) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴))) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))))
464, 38, 44, 45syl3anc 1372 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴))) = ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))))
47 uncom 4043 . . . . . . . 8 ((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴)) = ( (ω ∖ 𝐴) ∪ (𝐴 (ω ∖ 𝐴)))
48 onnmin 7537 . . . . . . . . . . . . . . 15 (((ω ∖ 𝐴) ⊆ On ∧ 𝑎 ∈ (ω ∖ 𝐴)) → ¬ 𝑎 (ω ∖ 𝐴))
497, 48mpan 690 . . . . . . . . . . . . . 14 (𝑎 ∈ (ω ∖ 𝐴) → ¬ 𝑎 (ω ∖ 𝐴))
5049con2i 141 . . . . . . . . . . . . 13 (𝑎 (ω ∖ 𝐴) → ¬ 𝑎 ∈ (ω ∖ 𝐴))
5150adantl 485 . . . . . . . . . . . 12 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 (ω ∖ 𝐴)) → ¬ 𝑎 ∈ (ω ∖ 𝐴))
52 ordom 7608 . . . . . . . . . . . . . . 15 Ord ω
53 ordelss 6188 . . . . . . . . . . . . . . 15 ((Ord ω ∧ (ω ∖ 𝐴) ∈ ω) → (ω ∖ 𝐴) ⊆ ω)
5452, 19, 53sylancr 590 . . . . . . . . . . . . . 14 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ⊆ ω)
5554sselda 3877 . . . . . . . . . . . . 13 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 (ω ∖ 𝐴)) → 𝑎 ∈ ω)
56 eldif 3853 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (ω ∖ 𝐴) ↔ (𝑎 ∈ ω ∧ ¬ 𝑎𝐴))
5756simplbi2 504 . . . . . . . . . . . . . . 15 (𝑎 ∈ ω → (¬ 𝑎𝐴𝑎 ∈ (ω ∖ 𝐴)))
5857orrd 862 . . . . . . . . . . . . . 14 (𝑎 ∈ ω → (𝑎𝐴𝑎 ∈ (ω ∖ 𝐴)))
5958orcomd 870 . . . . . . . . . . . . 13 (𝑎 ∈ ω → (𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎𝐴))
6055, 59syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 (ω ∖ 𝐴)) → (𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎𝐴))
61 orel1 888 . . . . . . . . . . . 12 𝑎 ∈ (ω ∖ 𝐴) → ((𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎𝐴) → 𝑎𝐴))
6251, 60, 61sylc 65 . . . . . . . . . . 11 ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 (ω ∖ 𝐴)) → 𝑎𝐴)
6362ex 416 . . . . . . . . . 10 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝑎 (ω ∖ 𝐴) → 𝑎𝐴))
6463ssrdv 3883 . . . . . . . . 9 (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ⊆ 𝐴)
65 undif 4371 . . . . . . . . 9 ( (ω ∖ 𝐴) ⊆ 𝐴 ↔ ( (ω ∖ 𝐴) ∪ (𝐴 (ω ∖ 𝐴))) = 𝐴)
6664, 65sylib 221 . . . . . . . 8 (𝐴 ∈ (𝒫 ω ∩ Fin) → ( (ω ∖ 𝐴) ∪ (𝐴 (ω ∖ 𝐴))) = 𝐴)
6747, 66syl5eq 2785 . . . . . . 7 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴)) = 𝐴)
6867fveq2d 6678 . . . . . 6 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ (ω ∖ 𝐴))) = (𝐹𝐴))
6946, 68eqtr3d 2775 . . . . 5 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))) = (𝐹𝐴))
70 suceq 6237 . . . . 5 (((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))) = (𝐹𝐴) → suc ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))) = suc (𝐹𝐴))
7169, 70syl 17 . . . 4 (𝐴 ∈ (𝒫 ω ∩ Fin) → suc ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o (𝐹 (ω ∖ 𝐴))) = suc (𝐹𝐴))
7242, 71eqtrd 2773 . . 3 (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 (ω ∖ 𝐴))) +o suc (𝐹 (ω ∖ 𝐴))) = suc (𝐹𝐴))
7330, 33, 723eqtrd 2777 . 2 (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = suc (𝐹𝐴))
74 fveqeq2 6683 . . 3 (𝑏 = ((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)}) → ((𝐹𝑏) = suc (𝐹𝐴) ↔ (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = suc (𝐹𝐴)))
7574rspcev 3526 . 2 ((((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin) ∧ (𝐹‘((𝐴 (ω ∖ 𝐴)) ∪ { (ω ∖ 𝐴)})) = suc (𝐹𝐴)) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹𝑏) = suc (𝐹𝐴))
7623, 73, 75syl2anc 587 1 (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹𝑏) = suc (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 846   = wceq 1542  wcel 2114  wne 2934  wrex 3054  cdif 3840  cun 3841  cin 3842  wss 3843  c0 4211  𝒫 cpw 4488  {csn 4516   cint 4836   ciun 4881  cmpt 5110   × cxp 5523  Ord word 6171  Oncon0 6172  suc csuc 6174  cfv 6339  (class class class)co 7170  ωcom 7599   +o coa 8128  Fincfn 8555  cardccrd 9437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-1st 7714  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-2o 8132  df-oadd 8135  df-er 8320  df-map 8439  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-dju 9403  df-card 9441
This theorem is referenced by:  ackbij1  9738
  Copyright terms: Public domain W3C validator