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 syl6eq ⊢ ( 𝑏 = ∅ → ( 𝑏 ∪ { 𝑐 } ) = { 𝑐 } )
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 𝐴 ) → ∪ 𝐴 ∈ 𝐴 )