This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pgpfac1lem1

Description: Lemma for pgpfac1 . (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses pgpfac1.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
pgpfac1.s ⊢ 𝑆 = ( 𝐾 ‘ { 𝐴 } )
pgpfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
pgpfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
pgpfac1.e ⊢ 𝐸 = ( gEx ‘ 𝐺 )
pgpfac1.z ⊢ 0 = ( 0g ‘ 𝐺 )
pgpfac1.l ⊢ ⊕ = ( LSSum ‘ 𝐺 )
pgpfac1.p ⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
pgpfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
pgpfac1.n ⊢ ( 𝜑 → 𝐵 ∈ Fin )
pgpfac1.oe ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
pgpfac1.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
pgpfac1.au ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
pgpfac1.w ⊢ ( 𝜑 → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
pgpfac1.i ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑊 ) = { 0 } )
pgpfac1.ss ⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 )
pgpfac1.2 ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ) )
Assertion pgpfac1lem1 ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 pgpfac1.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
2 pgpfac1.s ⊢ 𝑆 = ( 𝐾 ‘ { 𝐴 } )
3 pgpfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 pgpfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
5 pgpfac1.e ⊢ 𝐸 = ( gEx ‘ 𝐺 )
6 pgpfac1.z ⊢ 0 = ( 0g ‘ 𝐺 )
7 pgpfac1.l ⊢ ⊕ = ( LSSum ‘ 𝐺 )
8 pgpfac1.p ⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
9 pgpfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
10 pgpfac1.n ⊢ ( 𝜑 → 𝐵 ∈ Fin )
11 pgpfac1.oe ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
12 pgpfac1.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
13 pgpfac1.au ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
14 pgpfac1.w ⊢ ( 𝜑 → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
15 pgpfac1.i ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑊 ) = { 0 } )
16 pgpfac1.ss ⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 )
17 pgpfac1.2 ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ) )
18 16 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 )
19 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
20 3 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
21 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
22 9 19 20 21 4syl ⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
24 eldifi ⊢ ( 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) → 𝐶 ∈ 𝑈 )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → 𝐶 ∈ 𝑈 )
26 25 snssd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → { 𝐶 } ⊆ 𝑈 )
27 12 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
28 1 mrcsscl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ { 𝐶 } ⊆ 𝑈 ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐾 ‘ { 𝐶 } ) ⊆ 𝑈 )
29 23 26 27 28 syl3anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( 𝐾 ‘ { 𝐶 } ) ⊆ 𝑈 )
30 3 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
31 12 30 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
32 31 13 sseldd ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
33 1 mrcsncl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
34 22 32 33 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
35 2 34 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
36 7 lsmsubg2 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
37 9 35 14 36 syl3anc ⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
39 31 sselda ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) → 𝐶 ∈ 𝐵 )
40 24 39 sylan2 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → 𝐶 ∈ 𝐵 )
41 1 mrcsncl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐶 } ) ∈ ( SubGrp ‘ 𝐺 ) )
42 23 40 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( 𝐾 ‘ { 𝐶 } ) ∈ ( SubGrp ‘ 𝐺 ) )
43 7 lsmlub ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝐶 } ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 ∧ ( 𝐾 ‘ { 𝐶 } ) ⊆ 𝑈 ) ↔ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊆ 𝑈 ) )
44 38 42 27 43 syl3anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 ∧ ( 𝐾 ‘ { 𝐶 } ) ⊆ 𝑈 ) ↔ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊆ 𝑈 ) )
45 18 29 44 mpbi2and ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊆ 𝑈 )
46 7 lsmub1 ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝐶 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 ⊕ 𝑊 ) ⊆ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) )
47 38 42 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( 𝑆 ⊕ 𝑊 ) ⊆ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) )
48 7 lsmub2 ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝐶 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐾 ‘ { 𝐶 } ) ⊆ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) )
49 38 42 48 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( 𝐾 ‘ { 𝐶 } ) ⊆ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) )
50 40 snssd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → { 𝐶 } ⊆ 𝐵 )
51 23 1 50 mrcssidd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → { 𝐶 } ⊆ ( 𝐾 ‘ { 𝐶 } ) )
52 snssg ⊢ ( 𝐶 ∈ 𝐵 → ( 𝐶 ∈ ( 𝐾 ‘ { 𝐶 } ) ↔ { 𝐶 } ⊆ ( 𝐾 ‘ { 𝐶 } ) ) )
53 40 52 syl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( 𝐶 ∈ ( 𝐾 ‘ { 𝐶 } ) ↔ { 𝐶 } ⊆ ( 𝐾 ‘ { 𝐶 } ) ) )
54 51 53 mpbird ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → 𝐶 ∈ ( 𝐾 ‘ { 𝐶 } ) )
55 49 54 sseldd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → 𝐶 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) )
56 eldifn ⊢ ( 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) → ¬ 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) )
57 56 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ¬ 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) )
58 47 55 57 ssnelpssd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( 𝑆 ⊕ 𝑊 ) ⊊ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) )
59 7 lsmub1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( 𝑆 ⊕ 𝑊 ) )
60 35 14 59 syl2anc ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑆 ⊕ 𝑊 ) )
61 32 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝐵 )
62 22 1 61 mrcssidd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) )
63 62 2 sseqtrrdi ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑆 )
64 snssg ⊢ ( 𝐴 ∈ 𝑈 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
65 13 64 syl ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
66 63 65 mpbird ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
67 60 66 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ⊕ 𝑊 ) )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → 𝐴 ∈ ( 𝑆 ⊕ 𝑊 ) )
69 47 68 sseldd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → 𝐴 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) )
70 psseq1 ⊢ ( 𝑤 = ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) → ( 𝑤 ⊊ 𝑈 ↔ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊊ 𝑈 ) )
71 eleq2 ⊢ ( 𝑤 = ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) → ( 𝐴 ∈ 𝑤 ↔ 𝐴 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ) )
72 70 71 anbi12d ⊢ ( 𝑤 = ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) → ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) ↔ ( ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊊ 𝑈 ∧ 𝐴 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ) ) )
73 psseq2 ⊢ ( 𝑤 = ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ↔ ( 𝑆 ⊕ 𝑊 ) ⊊ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ) )
74 73 notbid ⊢ ( 𝑤 = ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) → ( ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ↔ ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ) )
75 72 74 imbi12d ⊢ ( 𝑤 = ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) → ( ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ) ↔ ( ( ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊊ 𝑈 ∧ 𝐴 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ) ) )
76 17 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ) )
77 9 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → 𝐺 ∈ Abel )
78 7 lsmsubg2 ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝐶 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ∈ ( SubGrp ‘ 𝐺 ) )
79 77 38 42 78 syl3anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ∈ ( SubGrp ‘ 𝐺 ) )
80 75 76 79 rspcdva ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊊ 𝑈 ∧ 𝐴 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ) )
81 69 80 mpan2d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊊ 𝑈 → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ) )
82 58 81 mt2d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ¬ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊊ 𝑈 )
83 npss ⊢ ( ¬ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊊ 𝑈 ↔ ( ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊆ 𝑈 → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) = 𝑈 ) )
84 82 83 sylib ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) ⊆ 𝑈 → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) = 𝑈 ) )
85 45 84 mpd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐶 } ) ) = 𝑈 )