Metamath Proof Explorer


Theorem fin1a2lem10

Description: Lemma for fin1a2 . A nonempty finite union of members of a chain is a member of the chain. (Contributed by Stefan O'Rear, 8-Nov-2014)

Ref Expression
Assertion fin1a2lem10 A A Fin [⊂] Or A A A

Proof

Step Hyp Ref Expression
1 eqneqall a = a [⊂] Or a a a
2 tru
3 2 a1i a =
4 1 3 2thd a = a [⊂] Or a a a
5 neeq1 a = b a b
6 soeq2 a = b [⊂] Or a [⊂] Or b
7 unieq a = b a = b
8 id a = b a = b
9 7 8 eleq12d a = b a a b b
10 6 9 imbi12d a = b [⊂] Or a a a [⊂] Or b b b
11 5 10 imbi12d a = b a [⊂] Or a a a b [⊂] Or b b b
12 neeq1 a = b c a b c
13 soeq2 a = b c [⊂] Or a [⊂] Or b c
14 unieq a = b c a = b c
15 id a = b c a = b c
16 14 15 eleq12d a = b c a a b c b c
17 13 16 imbi12d a = b c [⊂] Or a a a [⊂] Or b c b c b c
18 12 17 imbi12d a = b c a [⊂] Or a a a b c [⊂] Or b c b c b c
19 neeq1 a = A a A
20 soeq2 a = A [⊂] Or a [⊂] Or A
21 unieq a = A a = A
22 id a = A a = A
23 21 22 eleq12d a = A a a A A
24 20 23 imbi12d a = A [⊂] Or a a a [⊂] Or A A A
25 19 24 imbi12d a = A a [⊂] Or a a a A [⊂] Or A A A
26 vex c V
27 26 unisn c = c
28 vsnid c c
29 27 28 eqeltri c c
30 uneq1 b = b c = c
31 uncom c = c
32 un0 c = c
33 31 32 eqtri c = c
34 30 33 eqtrdi b = b c = c
35 34 unieqd b = b c = c
36 35 34 eleq12d b = b c b c c c
37 29 36 mpbiri b = b c b c
38 37 a1d b = b [⊂] Or b b b b c b c
39 38 adantl b Fin [⊂] Or b c b c b = b [⊂] Or b b b b c b c
40 simpr b Fin [⊂] Or b c b c b b
41 ssun1 b b c
42 simpl2 b Fin [⊂] Or b c b c b [⊂] Or b c
43 soss b b c [⊂] Or b c [⊂] Or b
44 41 42 43 mpsyl b Fin [⊂] Or b c b c b [⊂] Or b
45 uniun b c = b c
46 27 uneq2i b c = b c
47 45 46 eqtri b c = b c
48 simprr b Fin [⊂] Or b c b c b b b b b
49 simpl2 b Fin [⊂] Or b c b c b b b [⊂] Or b c
50 elun1 b b b b c
51 50 ad2antll b Fin [⊂] Or b c b c b b b b b c
52 ssun2 c b c
53 52 28 sselii c b c
54 53 a1i b Fin [⊂] Or b c b c b b b c b c
55 sorpssi [⊂] Or b c b b c c b c b c c b
56 49 51 54 55 syl12anc b Fin [⊂] Or b c b c b b b b c c b
57 ssequn1 b c b c = c
58 53 a1i b b c b c
59 eleq1 b c = c b c b c c b c
60 58 59 syl5ibr b c = c b b b c b c
61 57 60 sylbi b c b b b c b c
62 61 impcom b b b c b c b c
63 uncom b c = c b
64 ssequn1 c b c b = b
65 eleq1 c b = b c b b c b b c
66 50 65 syl5ibr c b = b b b c b b c
67 64 66 sylbi c b b b c b b c
68 67 impcom b b c b c b b c
69 63 68 eqeltrid b b c b b c b c
70 62 69 jaodan b b b c c b b c b c
71 48 56 70 syl2anc b Fin [⊂] Or b c b c b b b b c b c
72 47 71 eqeltrid b Fin [⊂] Or b c b c b b b b c b c
73 72 expr b Fin [⊂] Or b c b c b b b b c b c
74 44 73 embantd b Fin [⊂] Or b c b c b [⊂] Or b b b b c b c
75 40 74 embantd b Fin [⊂] Or b c b c b b [⊂] Or b b b b c b c
76 39 75 pm2.61dane b Fin [⊂] Or b c b c b [⊂] Or b b b b c b c
77 76 3exp b Fin [⊂] Or b c b c b [⊂] Or b b b b c b c
78 77 com24 b Fin b [⊂] Or b b b b c [⊂] Or b c b c b c
79 4 11 18 25 2 78 findcard2 A Fin A [⊂] Or A A A
80 79 3imp21 A A Fin [⊂] Or A A A