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

Theorem fin1a2lem10 9423
Description: Lemma for fin1a2 9429. 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 2943 . . . . 5 (𝑎 = ∅ → (𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)))
2 tru 1636 . . . . . 6
32a1i 11 . . . . 5 (𝑎 = ∅ → ⊤)
41, 32thd 255 . . . 4 (𝑎 = ∅ → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ ⊤))
5 neeq1 2994 . . . . 5 (𝑎 = 𝑏 → (𝑎 ≠ ∅ ↔ 𝑏 ≠ ∅))
6 soeq2 5207 . . . . . 6 (𝑎 = 𝑏 → ( [] Or 𝑎 ↔ [] Or 𝑏))
7 unieq 4596 . . . . . . 7 (𝑎 = 𝑏 𝑎 = 𝑏)
8 id 22 . . . . . . 7 (𝑎 = 𝑏𝑎 = 𝑏)
97, 8eleq12d 2833 . . . . . 6 (𝑎 = 𝑏 → ( 𝑎𝑎 𝑏𝑏))
106, 9imbi12d 333 . . . . 5 (𝑎 = 𝑏 → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or 𝑏 𝑏𝑏)))
115, 10imbi12d 333 . . . 4 (𝑎 = 𝑏 → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ (𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏))))
12 neeq1 2994 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎 ≠ ∅ ↔ (𝑏 ∪ {𝑐}) ≠ ∅))
13 soeq2 5207 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → ( [] Or 𝑎 ↔ [] Or (𝑏 ∪ {𝑐})))
14 unieq 4596 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → 𝑎 = (𝑏 ∪ {𝑐}))
15 id 22 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → 𝑎 = (𝑏 ∪ {𝑐}))
1614, 15eleq12d 2833 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → ( 𝑎𝑎 (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
1713, 16imbi12d 333 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))))
1812, 17imbi12d 333 . . . 4 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
19 neeq1 2994 . . . . 5 (𝑎 = 𝐴 → (𝑎 ≠ ∅ ↔ 𝐴 ≠ ∅))
20 soeq2 5207 . . . . . 6 (𝑎 = 𝐴 → ( [] Or 𝑎 ↔ [] Or 𝐴))
21 unieq 4596 . . . . . . 7 (𝑎 = 𝐴 𝑎 = 𝐴)
22 id 22 . . . . . . 7 (𝑎 = 𝐴𝑎 = 𝐴)
2321, 22eleq12d 2833 . . . . . 6 (𝑎 = 𝐴 → ( 𝑎𝑎 𝐴𝐴))
2420, 23imbi12d 333 . . . . 5 (𝑎 = 𝐴 → (( [] Or 𝑎 𝑎𝑎) ↔ ( [] Or 𝐴 𝐴𝐴)))
2519, 24imbi12d 333 . . . 4 (𝑎 = 𝐴 → ((𝑎 ≠ ∅ → ( [] Or 𝑎 𝑎𝑎)) ↔ (𝐴 ≠ ∅ → ( [] Or 𝐴 𝐴𝐴))))
26 vex 3343 . . . . . . . . . . . 12 𝑐 ∈ V
2726unisn 4603 . . . . . . . . . . 11 {𝑐} = 𝑐
28 vsnid 4354 . . . . . . . . . . 11 𝑐 ∈ {𝑐}
2927, 28eqeltri 2835 . . . . . . . . . 10 {𝑐} ∈ {𝑐}
30 uneq1 3903 . . . . . . . . . . . . 13 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = (∅ ∪ {𝑐}))
31 uncom 3900 . . . . . . . . . . . . . 14 (∅ ∪ {𝑐}) = ({𝑐} ∪ ∅)
32 un0 4110 . . . . . . . . . . . . . 14 ({𝑐} ∪ ∅) = {𝑐}
3331, 32eqtri 2782 . . . . . . . . . . . . 13 (∅ ∪ {𝑐}) = {𝑐}
3430, 33syl6eq 2810 . . . . . . . . . . . 12 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = {𝑐})
3534unieqd 4598 . . . . . . . . . . 11 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = {𝑐})
3635, 34eleq12d 2833 . . . . . . . . . 10 (𝑏 = ∅ → ( (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}) ↔ {𝑐} ∈ {𝑐}))
3729, 36mpbiri 248 . . . . . . . . 9 (𝑏 = ∅ → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))
3837a1d 25 . . . . . . . 8 (𝑏 = ∅ → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
3938adantl 473 . . . . . . 7 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 = ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
40 simpr 479 . . . . . . . 8 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → 𝑏 ≠ ∅)
41 ssun1 3919 . . . . . . . . . 10 𝑏 ⊆ (𝑏 ∪ {𝑐})
42 simpl2 1230 . . . . . . . . . 10 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [] Or (𝑏 ∪ {𝑐}))
43 soss 5205 . . . . . . . . . 10 (𝑏 ⊆ (𝑏 ∪ {𝑐}) → ( [] Or (𝑏 ∪ {𝑐}) → [] Or 𝑏))
4441, 42, 43mpsyl 68 . . . . . . . . 9 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [] Or 𝑏)
45 uniun 4608 . . . . . . . . . . . 12 (𝑏 ∪ {𝑐}) = ( 𝑏 {𝑐})
4627uneq2i 3907 . . . . . . . . . . . 12 ( 𝑏 {𝑐}) = ( 𝑏𝑐)
4745, 46eqtri 2782 . . . . . . . . . . 11 (𝑏 ∪ {𝑐}) = ( 𝑏𝑐)
48 simprr 813 . . . . . . . . . . . 12 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑏𝑏)
49 simpl2 1230 . . . . . . . . . . . . 13 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → [] Or (𝑏 ∪ {𝑐}))
50 elun1 3923 . . . . . . . . . . . . . 14 ( 𝑏𝑏 𝑏 ∈ (𝑏 ∪ {𝑐}))
5150ad2antll 767 . . . . . . . . . . . . 13 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑏 ∈ (𝑏 ∪ {𝑐}))
52 ssun2 3920 . . . . . . . . . . . . . . 15 {𝑐} ⊆ (𝑏 ∪ {𝑐})
5352, 28sselii 3741 . . . . . . . . . . . . . 14 𝑐 ∈ (𝑏 ∪ {𝑐})
5453a1i 11 . . . . . . . . . . . . 13 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → 𝑐 ∈ (𝑏 ∪ {𝑐}))
55 sorpssi 7108 . . . . . . . . . . . . 13 (( [] Or (𝑏 ∪ {𝑐}) ∧ ( 𝑏 ∈ (𝑏 ∪ {𝑐}) ∧ 𝑐 ∈ (𝑏 ∪ {𝑐}))) → ( 𝑏𝑐𝑐 𝑏))
5649, 51, 54, 55syl12anc 1475 . . . . . . . . . . . 12 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → ( 𝑏𝑐𝑐 𝑏))
57 ssequn1 3926 . . . . . . . . . . . . . . 15 ( 𝑏𝑐 ↔ ( 𝑏𝑐) = 𝑐)
5853a1i 11 . . . . . . . . . . . . . . . 16 ( 𝑏𝑏𝑐 ∈ (𝑏 ∪ {𝑐}))
59 eleq1 2827 . . . . . . . . . . . . . . . 16 (( 𝑏𝑐) = 𝑐 → (( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}) ↔ 𝑐 ∈ (𝑏 ∪ {𝑐})))
6058, 59syl5ibr 236 . . . . . . . . . . . . . . 15 (( 𝑏𝑐) = 𝑐 → ( 𝑏𝑏 → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐})))
6157, 60sylbi 207 . . . . . . . . . . . . . 14 ( 𝑏𝑐 → ( 𝑏𝑏 → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐})))
6261impcom 445 . . . . . . . . . . . . 13 (( 𝑏𝑏 𝑏𝑐) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
63 uncom 3900 . . . . . . . . . . . . . 14 ( 𝑏𝑐) = (𝑐 𝑏)
64 ssequn1 3926 . . . . . . . . . . . . . . . 16 (𝑐 𝑏 ↔ (𝑐 𝑏) = 𝑏)
65 eleq1 2827 . . . . . . . . . . . . . . . . 17 ((𝑐 𝑏) = 𝑏 → ((𝑐 𝑏) ∈ (𝑏 ∪ {𝑐}) ↔ 𝑏 ∈ (𝑏 ∪ {𝑐})))
6650, 65syl5ibr 236 . . . . . . . . . . . . . . . 16 ((𝑐 𝑏) = 𝑏 → ( 𝑏𝑏 → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐})))
6764, 66sylbi 207 . . . . . . . . . . . . . . 15 (𝑐 𝑏 → ( 𝑏𝑏 → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐})))
6867impcom 445 . . . . . . . . . . . . . 14 (( 𝑏𝑏𝑐 𝑏) → (𝑐 𝑏) ∈ (𝑏 ∪ {𝑐}))
6963, 68syl5eqel 2843 . . . . . . . . . . . . 13 (( 𝑏𝑏𝑐 𝑏) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7062, 69jaodan 861 . . . . . . . . . . . 12 (( 𝑏𝑏 ∧ ( 𝑏𝑐𝑐 𝑏)) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7148, 56, 70syl2anc 696 . . . . . . . . . . 11 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → ( 𝑏𝑐) ∈ (𝑏 ∪ {𝑐}))
7247, 71syl5eqel 2843 . . . . . . . . . 10 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))
7372expr 644 . . . . . . . . 9 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → ( 𝑏𝑏 (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7444, 73embantd 59 . . . . . . . 8 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → (( [] Or 𝑏 𝑏𝑏) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7540, 74embantd 59 . . . . . . 7 (((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
7639, 75pm2.61dane 3019 . . . . . 6 ((𝑏 ∈ Fin ∧ [] Or (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))
77763exp 1113 . . . . 5 (𝑏 ∈ Fin → ( [] Or (𝑏 ∪ {𝑐}) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
7877com24 95 . . . 4 (𝑏 ∈ Fin → ((𝑏 ≠ ∅ → ( [] Or 𝑏 𝑏𝑏)) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [] Or (𝑏 ∪ {𝑐}) → (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))))
794, 11, 18, 25, 2, 78findcard2 8365 . . 3 (𝐴 ∈ Fin → (𝐴 ≠ ∅ → ( [] Or 𝐴 𝐴𝐴)))
8079com12 32 . 2 (𝐴 ≠ ∅ → (𝐴 ∈ Fin → ( [] Or 𝐴 𝐴𝐴)))
81803imp 1102 1 ((𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧ [] Or 𝐴) → 𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383  w3a 1072   = wceq 1632  wtru 1633  wcel 2139  wne 2932  cun 3713  wss 3715  c0 4058  {csn 4321   cuni 4588   Or wor 5186   [] crpss 7101  Fincfn 8121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-rpss 7102  df-om 7231  df-1o 7729  df-er 7911  df-en 8122  df-fin 8125
This theorem is referenced by:  fin1a2lem11  9424  pgpfac1lem5  18678
  Copyright terms: Public domain W3C validator