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

Theorem fin1a2lem10 9484
Description: Lemma for fin1a2 9490. 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 2948 . . . . 5 (𝑎 = ∅ → (𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)))
2 tru 1657 . . . . . 6
32a1i 11 . . . . 5 (𝑎 = ∅ → ⊤)
41, 32thd 256 . . . 4 (𝑎 = ∅ → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ ⊤))
5 neeq1 2999 . . . . 5 (𝑎 = 𝑏 → (𝑎 ≠ ∅ ↔ 𝑏 ≠ ∅))
6 soeq2 5218 . . . . . 6 (𝑎 = 𝑏 → ( [] Or 𝑎 ↔ [] Or 𝑏))
7 unieq 4602 . . . . . . 7 (𝑎 = 𝑏 𝑎 = 𝑏)
8 id 22 . . . . . . 7 (𝑎 = 𝑏𝑎 = 𝑏)
97, 8eleq12d 2838 . . . . . 6 (𝑎 = 𝑏 → ( 𝑎𝑎 𝑏𝑏))
106, 9imbi12d 335 . . . . 5 (𝑎 = 𝑏 → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or 𝑏 𝑏𝑏)))
115, 10imbi12d 335 . . . 4 (𝑎 = 𝑏 → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ (𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏))))
12 neeq1 2999 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎 ≠ ∅ ↔ (𝑏 ∪ {𝑐}) ≠ ∅))
13 soeq2 5218 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → ( [] Or 𝑎 ↔ [] Or (𝑏 ∪ {𝑐})))
14 unieq 4602 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → 𝑎 = (𝑏 ∪ {𝑐}))
15 id 22 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → 𝑎 = (𝑏 ∪ {𝑐}))
1614, 15eleq12d 2838 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → ( 𝑎𝑎 (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
1713, 16imbi12d 335 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))))
1812, 17imbi12d 335 . . . 4 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
19 neeq1 2999 . . . . 5 (𝑎 = 𝐴 → (𝑎 ≠ ∅ ↔ 𝐴 ≠ ∅))
20 soeq2 5218 . . . . . 6 (𝑎 = 𝐴 → ( [] Or 𝑎 ↔ [] Or 𝐴))
21 unieq 4602 . . . . . . 7 (𝑎 = 𝐴 𝑎 = 𝐴)
22 id 22 . . . . . . 7 (𝑎 = 𝐴𝑎 = 𝐴)
2321, 22eleq12d 2838 . . . . . 6 (𝑎 = 𝐴 → ( 𝑎𝑎 𝐴𝐴))
2420, 23imbi12d 335 . . . . 5 (𝑎 = 𝐴 → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or 𝐴 𝐴𝐴)))
2519, 24imbi12d 335 . . . 4 (𝑎 = 𝐴 → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ (𝐴 ≠ ∅ → ( [] Or 𝐴 𝐴𝐴))))
26 vex 3353 . . . . . . . . . . . 12 𝑐 ∈ V
2726unisn 4610 . . . . . . . . . . 11 {𝑐} = 𝑐
28 vsnid 4367 . . . . . . . . . . 11 𝑐 ∈ {𝑐}
2927, 28eqeltri 2840 . . . . . . . . . 10 {𝑐} ∈ {𝑐}
30 uneq1 3922 . . . . . . . . . . . . 13 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = (∅ ∪ {𝑐}))
31 uncom 3919 . . . . . . . . . . . . . 14 (∅ ∪ {𝑐}) = ({𝑐} ∪ ∅)
32 un0 4129 . . . . . . . . . . . . . 14 ({𝑐} ∪ ∅) = {𝑐}
3331, 32eqtri 2787 . . . . . . . . . . . . 13 (∅ ∪ {𝑐}) = {𝑐}
3430, 33syl6eq 2815 . . . . . . . . . . . 12 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = {𝑐})
3534unieqd 4604 . . . . . . . . . . 11 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = {𝑐})
3635, 34eleq12d 2838 . . . . . . . . . 10 (𝑏 = ∅ → ( (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}) ↔ {𝑐} ∈ {𝑐}))
3729, 36mpbiri 249 . . . . . . . . 9 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))
3837a1d 25 . . . . . . . 8 (𝑏 = ∅ → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
3938adantl 473 . . . . . . 7 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 = ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
40 simpr 477 . . . . . . . 8 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → 𝑏 ≠ ∅)
41 ssun1 3938 . . . . . . . . . 10 𝑏 ⊆ (𝑏 ∪ {𝑐})
42 simpl2 1244 . . . . . . . . . 10 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [] Or (𝑏 ∪ {𝑐}))
43 soss 5216 . . . . . . . . . 10 (𝑏 ⊆ (𝑏 ∪ {𝑐}) → ( [] Or (𝑏 ∪ {𝑐}) → [] Or 𝑏))
4441, 42, 43mpsyl 68 . . . . . . . . 9 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [] Or 𝑏)
45 uniun 4615 . . . . . . . . . . . 12 (𝑏 ∪ {𝑐}) = ( 𝑏 {𝑐})
4627uneq2i 3926 . . . . . . . . . . . 12 ( 𝑏 {𝑐}) = ( 𝑏𝑐)
4745, 46eqtri 2787 . . . . . . . . . . 11 (𝑏 ∪ {𝑐}) = ( 𝑏𝑐)
48 simprr 789 . . . . . . . . . . . 12 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑏𝑏)
49 simpl2 1244 . . . . . . . . . . . . 13 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → [] Or (𝑏 ∪ {𝑐}))
50 elun1 3942 . . . . . . . . . . . . . 14 ( 𝑏𝑏 𝑏 ∈ (𝑏 ∪ {𝑐}))
5150ad2antll 720 . . . . . . . . . . . . 13 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑏 ∈ (𝑏 ∪ {𝑐}))
52 ssun2 3939 . . . . . . . . . . . . . . 15 {𝑐} ⊆ (𝑏 ∪ {𝑐})
5352, 28sselii 3758 . . . . . . . . . . . . . 14 𝑐 ∈ (𝑏 ∪ {𝑐})
5453a1i 11 . . . . . . . . . . . . 13 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑐 ∈ (𝑏 ∪ {𝑐}))
55 sorpssi 7141 . . . . . . . . . . . . 13 (( [] Or (𝑏 ∪ {𝑐}) ∧ ( 𝑏 ∈ (𝑏 ∪ {𝑐}) ∧ 𝑐 ∈ (𝑏 ∪ {𝑐}))) → ( 𝑏𝑐𝑐 𝑏))
5649, 51, 54, 55syl12anc 865 . . . . . . . . . . . 12 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → ( 𝑏𝑐𝑐 𝑏))
57 ssequn1 3945 . . . . . . . . . . . . . . 15 ( 𝑏𝑐 ↔ ( 𝑏𝑐) = 𝑐)
5853a1i 11 . . . . . . . . . . . . . . . 16 ( 𝑏𝑏𝑐 ∈ (𝑏 ∪ {𝑐}))
59 eleq1 2832 . . . . . . . . . . . . . . . 16 (( 𝑏𝑐) = 𝑐 → (( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}) ↔ 𝑐 ∈ (𝑏 ∪ {𝑐})))
6058, 59syl5ibr 237 . . . . . . . . . . . . . . 15 (( 𝑏𝑐) = 𝑐 → ( 𝑏𝑏 → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐})))
6157, 60sylbi 208 . . . . . . . . . . . . . 14 ( 𝑏𝑐 → ( 𝑏𝑏 → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐})))
6261impcom 396 . . . . . . . . . . . . 13 (( 𝑏𝑏 𝑏𝑐) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
63 uncom 3919 . . . . . . . . . . . . . 14 ( 𝑏𝑐) = (𝑐 𝑏)
64 ssequn1 3945 . . . . . . . . . . . . . . . 16 (𝑐 𝑏 ↔ (𝑐 𝑏) = 𝑏)
65 eleq1 2832 . . . . . . . . . . . . . . . . 17 ((𝑐 𝑏) = 𝑏 → ((𝑐 𝑏) ∈ (𝑏 ∪ {𝑐}) ↔ 𝑏 ∈ (𝑏 ∪ {𝑐})))
6650, 65syl5ibr 237 . . . . . . . . . . . . . . . 16 ((𝑐 𝑏) = 𝑏 → ( 𝑏𝑏 → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐})))
6764, 66sylbi 208 . . . . . . . . . . . . . . 15 (𝑐 𝑏 → ( 𝑏𝑏 → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐})))
6867impcom 396 . . . . . . . . . . . . . 14 (( 𝑏𝑏𝑐 𝑏) → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐}))
6963, 68syl5eqel 2848 . . . . . . . . . . . . 13 (( 𝑏𝑏𝑐 𝑏) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7062, 69jaodan 980 . . . . . . . . . . . 12 (( 𝑏𝑏 ∧ ( 𝑏𝑐𝑐 𝑏)) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7148, 56, 70syl2anc 579 . . . . . . . . . . 11 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7247, 71syl5eqel 2848 . . . . . . . . . 10 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))
7372expr 448 . . . . . . . . 9 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → ( 𝑏𝑏 (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7444, 73embantd 59 . . . . . . . 8 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → (( [] Or 𝑏 𝑏𝑏) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7540, 74embantd 59 . . . . . . 7 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7639, 75pm2.61dane 3024 . . . . . 6 ((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
77763exp 1148 . . . . 5 (𝑏 ∈ Fin → ( [] Or (𝑏 ∪ {𝑐}) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
7877com24 95 . . . 4 (𝑏 ∈ Fin → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
794, 11, 18, 25, 2, 78findcard2 8407 . . 3 (𝐴 ∈ Fin → (𝐴 ≠ ∅ → ( [] Or 𝐴 𝐴𝐴)))
8079com12 32 . 2 (𝐴 ≠ ∅ → (𝐴 ∈ Fin → ( [] Or 𝐴 𝐴𝐴)))
81803imp 1137 1 ((𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧ [] Or 𝐴) → 𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wo 873  w3a 1107   = wceq 1652  wtru 1653  wcel 2155  wne 2937  cun 3730  wss 3732  c0 4079  {csn 4334   cuni 4594   Or wor 5197   [] crpss 7134  Fincfn 8160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-rpss 7135  df-om 7264  df-1o 7764  df-er 7947  df-en 8161  df-fin 8164
This theorem is referenced by:  fin1a2lem11  9485  pgpfac1lem5  18745
  Copyright terms: Public domain W3C validator