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 ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧ [] Or 𝐴 ) → 𝐴𝐴 )

Proof

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