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

Theorem fin1a2lem10 9182
Description: Lemma for fin1a2 9188. A nonempty finite union of members of a chain is a member of the chain. (Contributed by Stefan O'Rear, 8-Nov-2014.)
Assertion
Ref Expression
fin1a2lem10 ((𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧ [] Or 𝐴) → 𝐴𝐴)

Proof of Theorem fin1a2lem10
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqneqall 2801 . . . . 5 (𝑎 = ∅ → (𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)))
2 tru 1484 . . . . . 6
32a1i 11 . . . . 5 (𝑎 = ∅ → ⊤)
41, 32thd 255 . . . 4 (𝑎 = ∅ → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ ⊤))
5 neeq1 2852 . . . . 5 (𝑎 = 𝑏 → (𝑎 ≠ ∅ ↔ 𝑏 ≠ ∅))
6 soeq2 5020 . . . . . 6 (𝑎 = 𝑏 → ( [] Or 𝑎 ↔ [] Or 𝑏))
7 unieq 4415 . . . . . . 7 (𝑎 = 𝑏 𝑎 = 𝑏)
8 id 22 . . . . . . 7 (𝑎 = 𝑏𝑎 = 𝑏)
97, 8eleq12d 2692 . . . . . 6 (𝑎 = 𝑏 → ( 𝑎𝑎 𝑏𝑏))
106, 9imbi12d 334 . . . . 5 (𝑎 = 𝑏 → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or 𝑏 𝑏𝑏)))
115, 10imbi12d 334 . . . 4 (𝑎 = 𝑏 → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ (𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏))))
12 neeq1 2852 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎 ≠ ∅ ↔ (𝑏 ∪ {𝑐}) ≠ ∅))
13 soeq2 5020 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → ( [] Or 𝑎 ↔ [] Or (𝑏 ∪ {𝑐})))
14 unieq 4415 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → 𝑎 = (𝑏 ∪ {𝑐}))
15 id 22 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → 𝑎 = (𝑏 ∪ {𝑐}))
1614, 15eleq12d 2692 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → ( 𝑎𝑎 (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
1713, 16imbi12d 334 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))))
1812, 17imbi12d 334 . . . 4 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
19 neeq1 2852 . . . . 5 (𝑎 = 𝐴 → (𝑎 ≠ ∅ ↔ 𝐴 ≠ ∅))
20 soeq2 5020 . . . . . 6 (𝑎 = 𝐴 → ( [] Or 𝑎 ↔ [] Or 𝐴))
21 unieq 4415 . . . . . . 7 (𝑎 = 𝐴 𝑎 = 𝐴)
22 id 22 . . . . . . 7 (𝑎 = 𝐴𝑎 = 𝐴)
2321, 22eleq12d 2692 . . . . . 6 (𝑎 = 𝐴 → ( 𝑎𝑎 𝐴𝐴))
2420, 23imbi12d 334 . . . . 5 (𝑎 = 𝐴 → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or 𝐴 𝐴𝐴)))
2519, 24imbi12d 334 . . . 4 (𝑎 = 𝐴 → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ (𝐴 ≠ ∅ → ( [] Or 𝐴 𝐴𝐴))))
26 vex 3192 . . . . . . . . . . . 12 𝑐 ∈ V
2726unisn 4422 . . . . . . . . . . 11 {𝑐} = 𝑐
28 vsnid 4185 . . . . . . . . . . 11 𝑐 ∈ {𝑐}
2927, 28eqeltri 2694 . . . . . . . . . 10 {𝑐} ∈ {𝑐}
30 uneq1 3743 . . . . . . . . . . . . 13 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = (∅ ∪ {𝑐}))
31 uncom 3740 . . . . . . . . . . . . . 14 (∅ ∪ {𝑐}) = ({𝑐} ∪ ∅)
32 un0 3944 . . . . . . . . . . . . . 14 ({𝑐} ∪ ∅) = {𝑐}
3331, 32eqtri 2643 . . . . . . . . . . . . 13 (∅ ∪ {𝑐}) = {𝑐}
3430, 33syl6eq 2671 . . . . . . . . . . . 12 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = {𝑐})
3534unieqd 4417 . . . . . . . . . . 11 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = {𝑐})
3635, 34eleq12d 2692 . . . . . . . . . 10 (𝑏 = ∅ → ( (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}) ↔ {𝑐} ∈ {𝑐}))
3729, 36mpbiri 248 . . . . . . . . 9 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))
3837a1d 25 . . . . . . . 8 (𝑏 = ∅ → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
3938adantl 482 . . . . . . 7 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 = ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
40 simpr 477 . . . . . . . 8 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → 𝑏 ≠ ∅)
41 ssun1 3759 . . . . . . . . . 10 𝑏 ⊆ (𝑏 ∪ {𝑐})
42 simpl2 1063 . . . . . . . . . 10 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [] Or (𝑏 ∪ {𝑐}))
43 soss 5018 . . . . . . . . . 10 (𝑏 ⊆ (𝑏 ∪ {𝑐}) → ( [] Or (𝑏 ∪ {𝑐}) → [] Or 𝑏))
4441, 42, 43mpsyl 68 . . . . . . . . 9 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [] Or 𝑏)
45 uniun 4427 . . . . . . . . . . . 12 (𝑏 ∪ {𝑐}) = ( 𝑏 {𝑐})
4627uneq2i 3747 . . . . . . . . . . . 12 ( 𝑏 {𝑐}) = ( 𝑏𝑐)
4745, 46eqtri 2643 . . . . . . . . . . 11 (𝑏 ∪ {𝑐}) = ( 𝑏𝑐)
48 simprr 795 . . . . . . . . . . . 12 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑏𝑏)
49 simpl2 1063 . . . . . . . . . . . . 13 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → [] Or (𝑏 ∪ {𝑐}))
50 elun1 3763 . . . . . . . . . . . . . 14 ( 𝑏𝑏 𝑏 ∈ (𝑏 ∪ {𝑐}))
5150ad2antll 764 . . . . . . . . . . . . 13 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑏 ∈ (𝑏 ∪ {𝑐}))
52 ssun2 3760 . . . . . . . . . . . . . . 15 {𝑐} ⊆ (𝑏 ∪ {𝑐})
5352, 28sselii 3584 . . . . . . . . . . . . . 14 𝑐 ∈ (𝑏 ∪ {𝑐})
5453a1i 11 . . . . . . . . . . . . 13 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑐 ∈ (𝑏 ∪ {𝑐}))
55 sorpssi 6903 . . . . . . . . . . . . 13 (( [] Or (𝑏 ∪ {𝑐}) ∧ ( 𝑏 ∈ (𝑏 ∪ {𝑐}) ∧ 𝑐 ∈ (𝑏 ∪ {𝑐}))) → ( 𝑏𝑐𝑐 𝑏))
5649, 51, 54, 55syl12anc 1321 . . . . . . . . . . . 12 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → ( 𝑏𝑐𝑐 𝑏))
57 ssequn1 3766 . . . . . . . . . . . . . . 15 ( 𝑏𝑐 ↔ ( 𝑏𝑐) = 𝑐)
5853a1i 11 . . . . . . . . . . . . . . . 16 ( 𝑏𝑏𝑐 ∈ (𝑏 ∪ {𝑐}))
59 eleq1 2686 . . . . . . . . . . . . . . . 16 (( 𝑏𝑐) = 𝑐 → (( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}) ↔ 𝑐 ∈ (𝑏 ∪ {𝑐})))
6058, 59syl5ibr 236 . . . . . . . . . . . . . . 15 (( 𝑏𝑐) = 𝑐 → ( 𝑏𝑏 → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐})))
6157, 60sylbi 207 . . . . . . . . . . . . . 14 ( 𝑏𝑐 → ( 𝑏𝑏 → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐})))
6261impcom 446 . . . . . . . . . . . . 13 (( 𝑏𝑏 𝑏𝑐) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
63 uncom 3740 . . . . . . . . . . . . . 14 ( 𝑏𝑐) = (𝑐 𝑏)
64 ssequn1 3766 . . . . . . . . . . . . . . . 16 (𝑐 𝑏 ↔ (𝑐 𝑏) = 𝑏)
65 eleq1 2686 . . . . . . . . . . . . . . . . 17 ((𝑐 𝑏) = 𝑏 → ((𝑐 𝑏) ∈ (𝑏 ∪ {𝑐}) ↔ 𝑏 ∈ (𝑏 ∪ {𝑐})))
6650, 65syl5ibr 236 . . . . . . . . . . . . . . . 16 ((𝑐 𝑏) = 𝑏 → ( 𝑏𝑏 → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐})))
6764, 66sylbi 207 . . . . . . . . . . . . . . 15 (𝑐 𝑏 → ( 𝑏𝑏 → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐})))
6867impcom 446 . . . . . . . . . . . . . 14 (( 𝑏𝑏𝑐 𝑏) → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐}))
6963, 68syl5eqel 2702 . . . . . . . . . . . . 13 (( 𝑏𝑏𝑐 𝑏) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7062, 69jaodan 825 . . . . . . . . . . . 12 (( 𝑏𝑏 ∧ ( 𝑏𝑐𝑐 𝑏)) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7148, 56, 70syl2anc 692 . . . . . . . . . . 11 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7247, 71syl5eqel 2702 . . . . . . . . . 10 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))
7372expr 642 . . . . . . . . 9 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → ( 𝑏𝑏 (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7444, 73embantd 59 . . . . . . . 8 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → (( [] Or 𝑏 𝑏𝑏) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7540, 74embantd 59 . . . . . . 7 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7639, 75pm2.61dane 2877 . . . . . 6 ((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
77763exp 1261 . . . . 5 (𝑏 ∈ Fin → ( [] Or (𝑏 ∪ {𝑐}) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
7877com24 95 . . . 4 (𝑏 ∈ Fin → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
794, 11, 18, 25, 2, 78findcard2 8151 . . 3 (𝐴 ∈ Fin → (𝐴 ≠ ∅ → ( [] Or 𝐴 𝐴𝐴)))
8079com12 32 . 2 (𝐴 ≠ ∅ → (𝐴 ∈ Fin → ( [] Or 𝐴 𝐴𝐴)))
81803imp 1254 1 ((𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧ [] Or 𝐴) → 𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383  wa 384  w3a 1036   = wceq 1480  wtru 1481  wcel 1987  wne 2790  cun 3557  wss 3559  c0 3896  {csn 4153   cuni 4407   Or wor 4999   [] crpss 6896  Fincfn 7906
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 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
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 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  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-br 4619  df-opab 4679  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-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-rpss 6897  df-om 7020  df-1o 7512  df-er 7694  df-en 7907  df-fin 7910
This theorem is referenced by:  fin1a2lem11  9183  pgpfac1lem5  18406
  Copyright terms: Public domain W3C validator