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

Theorem fin1a2lem10 9823
Description: Lemma for fin1a2 9829. 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 3031 . . . 4 (𝑎 = ∅ → (𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)))
2 tru 1534 . . . . 5
32a1i 11 . . . 4 (𝑎 = ∅ → ⊤)
41, 32thd 266 . . 3 (𝑎 = ∅ → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ ⊤))
5 neeq1 3082 . . . 4 (𝑎 = 𝑏 → (𝑎 ≠ ∅ ↔ 𝑏 ≠ ∅))
6 soeq2 5493 . . . . 5 (𝑎 = 𝑏 → ( [] Or 𝑎 ↔ [] Or 𝑏))
7 unieq 4844 . . . . . 6 (𝑎 = 𝑏 𝑎 = 𝑏)
8 id 22 . . . . . 6 (𝑎 = 𝑏𝑎 = 𝑏)
97, 8eleq12d 2911 . . . . 5 (𝑎 = 𝑏 → ( 𝑎𝑎 𝑏𝑏))
106, 9imbi12d 346 . . . 4 (𝑎 = 𝑏 → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or 𝑏 𝑏𝑏)))
115, 10imbi12d 346 . . 3 (𝑎 = 𝑏 → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ (𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏))))
12 neeq1 3082 . . . 4 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎 ≠ ∅ ↔ (𝑏 ∪ {𝑐}) ≠ ∅))
13 soeq2 5493 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → ( [] Or 𝑎 ↔ [] Or (𝑏 ∪ {𝑐})))
14 unieq 4844 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → 𝑎 = (𝑏 ∪ {𝑐}))
15 id 22 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → 𝑎 = (𝑏 ∪ {𝑐}))
1614, 15eleq12d 2911 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → ( 𝑎𝑎 (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
1713, 16imbi12d 346 . . . 4 (𝑎 = (𝑏 ∪ {𝑐}) → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))))
1812, 17imbi12d 346 . . 3 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
19 neeq1 3082 . . . 4 (𝑎 = 𝐴 → (𝑎 ≠ ∅ ↔ 𝐴 ≠ ∅))
20 soeq2 5493 . . . . 5 (𝑎 = 𝐴 → ( [] Or 𝑎 ↔ [] Or 𝐴))
21 unieq 4844 . . . . . 6 (𝑎 = 𝐴 𝑎 = 𝐴)
22 id 22 . . . . . 6 (𝑎 = 𝐴𝑎 = 𝐴)
2321, 22eleq12d 2911 . . . . 5 (𝑎 = 𝐴 → ( 𝑎𝑎 𝐴𝐴))
2420, 23imbi12d 346 . . . 4 (𝑎 = 𝐴 → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or 𝐴 𝐴𝐴)))
2519, 24imbi12d 346 . . 3 (𝑎 = 𝐴 → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ (𝐴 ≠ ∅ → ( [] Or 𝐴 𝐴𝐴))))
26 vex 3502 . . . . . . . . . . 11 𝑐 ∈ V
2726unisn 4852 . . . . . . . . . 10 {𝑐} = 𝑐
28 vsnid 4598 . . . . . . . . . 10 𝑐 ∈ {𝑐}
2927, 28eqeltri 2913 . . . . . . . . 9 {𝑐} ∈ {𝑐}
30 uneq1 4135 . . . . . . . . . . . 12 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = (∅ ∪ {𝑐}))
31 uncom 4132 . . . . . . . . . . . . 13 (∅ ∪ {𝑐}) = ({𝑐} ∪ ∅)
32 un0 4347 . . . . . . . . . . . . 13 ({𝑐} ∪ ∅) = {𝑐}
3331, 32eqtri 2848 . . . . . . . . . . . 12 (∅ ∪ {𝑐}) = {𝑐}
3430, 33syl6eq 2876 . . . . . . . . . . 11 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = {𝑐})
3534unieqd 4846 . . . . . . . . . 10 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = {𝑐})
3635, 34eleq12d 2911 . . . . . . . . 9 (𝑏 = ∅ → ( (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}) ↔ {𝑐} ∈ {𝑐}))
3729, 36mpbiri 259 . . . . . . . 8 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))
3837a1d 25 . . . . . . 7 (𝑏 = ∅ → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
3938adantl 482 . . . . . 6 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 = ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
40 simpr 485 . . . . . . 7 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → 𝑏 ≠ ∅)
41 ssun1 4151 . . . . . . . . 9 𝑏 ⊆ (𝑏 ∪ {𝑐})
42 simpl2 1186 . . . . . . . . 9 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [] Or (𝑏 ∪ {𝑐}))
43 soss 5491 . . . . . . . . 9 (𝑏 ⊆ (𝑏 ∪ {𝑐}) → ( [] Or (𝑏 ∪ {𝑐}) → [] Or 𝑏))
4441, 42, 43mpsyl 68 . . . . . . . 8 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [] Or 𝑏)
45 uniun 4855 . . . . . . . . . . 11 (𝑏 ∪ {𝑐}) = ( 𝑏 {𝑐})
4627uneq2i 4139 . . . . . . . . . . 11 ( 𝑏 {𝑐}) = ( 𝑏𝑐)
4745, 46eqtri 2848 . . . . . . . . . 10 (𝑏 ∪ {𝑐}) = ( 𝑏𝑐)
48 simprr 769 . . . . . . . . . . 11 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑏𝑏)
49 simpl2 1186 . . . . . . . . . . . 12 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → [] Or (𝑏 ∪ {𝑐}))
50 elun1 4155 . . . . . . . . . . . . 13 ( 𝑏𝑏 𝑏 ∈ (𝑏 ∪ {𝑐}))
5150ad2antll 725 . . . . . . . . . . . 12 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑏 ∈ (𝑏 ∪ {𝑐}))
52 ssun2 4152 . . . . . . . . . . . . . 14 {𝑐} ⊆ (𝑏 ∪ {𝑐})
5352, 28sselii 3967 . . . . . . . . . . . . 13 𝑐 ∈ (𝑏 ∪ {𝑐})
5453a1i 11 . . . . . . . . . . . 12 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑐 ∈ (𝑏 ∪ {𝑐}))
55 sorpssi 7448 . . . . . . . . . . . 12 (( [] Or (𝑏 ∪ {𝑐}) ∧ ( 𝑏 ∈ (𝑏 ∪ {𝑐}) ∧ 𝑐 ∈ (𝑏 ∪ {𝑐}))) → ( 𝑏𝑐𝑐 𝑏))
5649, 51, 54, 55syl12anc 834 . . . . . . . . . . 11 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → ( 𝑏𝑐𝑐 𝑏))
57 ssequn1 4159 . . . . . . . . . . . . . 14 ( 𝑏𝑐 ↔ ( 𝑏𝑐) = 𝑐)
5853a1i 11 . . . . . . . . . . . . . . 15 ( 𝑏𝑏𝑐 ∈ (𝑏 ∪ {𝑐}))
59 eleq1 2904 . . . . . . . . . . . . . . 15 (( 𝑏𝑐) = 𝑐 → (( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}) ↔ 𝑐 ∈ (𝑏 ∪ {𝑐})))
6058, 59syl5ibr 247 . . . . . . . . . . . . . 14 (( 𝑏𝑐) = 𝑐 → ( 𝑏𝑏 → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐})))
6157, 60sylbi 218 . . . . . . . . . . . . 13 ( 𝑏𝑐 → ( 𝑏𝑏 → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐})))
6261impcom 408 . . . . . . . . . . . 12 (( 𝑏𝑏 𝑏𝑐) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
63 uncom 4132 . . . . . . . . . . . . 13 ( 𝑏𝑐) = (𝑐 𝑏)
64 ssequn1 4159 . . . . . . . . . . . . . . 15 (𝑐 𝑏 ↔ (𝑐 𝑏) = 𝑏)
65 eleq1 2904 . . . . . . . . . . . . . . . 16 ((𝑐 𝑏) = 𝑏 → ((𝑐 𝑏) ∈ (𝑏 ∪ {𝑐}) ↔ 𝑏 ∈ (𝑏 ∪ {𝑐})))
6650, 65syl5ibr 247 . . . . . . . . . . . . . . 15 ((𝑐 𝑏) = 𝑏 → ( 𝑏𝑏 → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐})))
6764, 66sylbi 218 . . . . . . . . . . . . . 14 (𝑐 𝑏 → ( 𝑏𝑏 → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐})))
6867impcom 408 . . . . . . . . . . . . 13 (( 𝑏𝑏𝑐 𝑏) → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐}))
6963, 68eqeltrid 2921 . . . . . . . . . . . 12 (( 𝑏𝑏𝑐 𝑏) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7062, 69jaodan 953 . . . . . . . . . . 11 (( 𝑏𝑏 ∧ ( 𝑏𝑐𝑐 𝑏)) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7148, 56, 70syl2anc 584 . . . . . . . . . 10 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7247, 71eqeltrid 2921 . . . . . . . . 9 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))
7372expr 457 . . . . . . . 8 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → ( 𝑏𝑏 (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7444, 73embantd 59 . . . . . . 7 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → (( [] Or 𝑏 𝑏𝑏) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7540, 74embantd 59 . . . . . 6 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7639, 75pm2.61dane 3108 . . . . 5 ((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
77763exp 1113 . . . 4 (𝑏 ∈ Fin → ( [] Or (𝑏 ∪ {𝑐}) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
7877com24 95 . . 3 (𝑏 ∈ Fin → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
794, 11, 18, 25, 2, 78findcard2 8750 . 2 (𝐴 ∈ Fin → (𝐴 ≠ ∅ → ( [] Or 𝐴 𝐴𝐴)))
80793imp21 1108 1 ((𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧ [] Or 𝐴) → 𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 843  w3a 1081   = wceq 1530  wtru 1531  wcel 2107  wne 3020  cun 3937  wss 3939  c0 4294  {csn 4563   cuni 4836   Or wor 5471   [] crpss 7441  Fincfn 8501
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-rpss 7442  df-om 7572  df-1o 8096  df-er 8282  df-en 8502  df-fin 8505
This theorem is referenced by:  fin1a2lem11  9824  pgpfac1lem5  19123
  Copyright terms: Public domain W3C validator