Metamath Proof Explorer


Theorem pgpfac1lem5

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.3 ( 𝜑 → ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠𝑈𝐴𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ) )
Assertion pgpfac1lem5 ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) )

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.3 ( 𝜑 → ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠𝑈𝐴𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ) )
15 pwfi ( 𝐵 ∈ Fin ↔ 𝒫 𝐵 ∈ Fin )
16 10 15 sylib ( 𝜑 → 𝒫 𝐵 ∈ Fin )
17 16 adantr ( ( 𝜑𝑆𝑈 ) → 𝒫 𝐵 ∈ Fin )
18 3 subgss ( 𝑣 ∈ ( SubGrp ‘ 𝐺 ) → 𝑣𝐵 )
19 18 3ad2ant2 ( ( ( 𝜑𝑆𝑈 ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑣𝑈𝐴𝑣 ) ) → 𝑣𝐵 )
20 velpw ( 𝑣 ∈ 𝒫 𝐵𝑣𝐵 )
21 19 20 sylibr ( ( ( 𝜑𝑆𝑈 ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑣𝑈𝐴𝑣 ) ) → 𝑣 ∈ 𝒫 𝐵 )
22 21 rabssdv ( ( 𝜑𝑆𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ⊆ 𝒫 𝐵 )
23 17 22 ssfid ( ( 𝜑𝑆𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∈ Fin )
24 finnum ( { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∈ Fin → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∈ dom card )
25 23 24 syl ( ( 𝜑𝑆𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∈ dom card )
26 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
27 9 26 syl ( 𝜑𝐺 ∈ Grp )
28 3 subgacs ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
29 acsmre ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
30 27 28 29 3syl ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
31 3 subgss ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈𝐵 )
32 12 31 syl ( 𝜑𝑈𝐵 )
33 32 13 sseldd ( 𝜑𝐴𝐵 )
34 1 mrcsncl ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
35 30 33 34 syl2anc ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
36 2 35 eqeltrid ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
37 36 adantr ( ( 𝜑𝑆𝑈 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
38 simpr ( ( 𝜑𝑆𝑈 ) → 𝑆𝑈 )
39 13 snssd ( 𝜑 → { 𝐴 } ⊆ 𝑈 )
40 39 32 sstrd ( 𝜑 → { 𝐴 } ⊆ 𝐵 )
41 30 1 40 mrcssidd ( 𝜑 → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) )
42 41 2 sseqtrrdi ( 𝜑 → { 𝐴 } ⊆ 𝑆 )
43 snssg ( 𝐴𝐵 → ( 𝐴𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
44 33 43 syl ( 𝜑 → ( 𝐴𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
45 42 44 mpbird ( 𝜑𝐴𝑆 )
46 45 adantr ( ( 𝜑𝑆𝑈 ) → 𝐴𝑆 )
47 psseq1 ( 𝑣 = 𝑆 → ( 𝑣𝑈𝑆𝑈 ) )
48 eleq2 ( 𝑣 = 𝑆 → ( 𝐴𝑣𝐴𝑆 ) )
49 47 48 anbi12d ( 𝑣 = 𝑆 → ( ( 𝑣𝑈𝐴𝑣 ) ↔ ( 𝑆𝑈𝐴𝑆 ) ) )
50 49 rspcev ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑆𝑈𝐴𝑆 ) ) → ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑣𝑈𝐴𝑣 ) )
51 37 38 46 50 syl12anc ( ( 𝜑𝑆𝑈 ) → ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑣𝑈𝐴𝑣 ) )
52 rabn0 ( { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ≠ ∅ ↔ ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑣𝑈𝐴𝑣 ) )
53 51 52 sylibr ( ( 𝜑𝑆𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ≠ ∅ )
54 simpr1 ( ( ( 𝜑𝑆𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) ) → 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } )
55 simpr2 ( ( ( 𝜑𝑆𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) ) → 𝑢 ≠ ∅ )
56 23 adantr ( ( ( 𝜑𝑆𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∈ Fin )
57 56 54 ssfid ( ( ( 𝜑𝑆𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) ) → 𝑢 ∈ Fin )
58 simpr3 ( ( ( 𝜑𝑆𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) ) → [] Or 𝑢 )
59 fin1a2lem10 ( ( 𝑢 ≠ ∅ ∧ 𝑢 ∈ Fin ∧ [] Or 𝑢 ) → 𝑢𝑢 )
60 55 57 58 59 syl3anc ( ( ( 𝜑𝑆𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) ) → 𝑢𝑢 )
61 54 60 sseldd ( ( ( 𝜑𝑆𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) ) → 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } )
62 61 ex ( ( 𝜑𝑆𝑈 ) → ( ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) → 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ) )
63 62 alrimiv ( ( 𝜑𝑆𝑈 ) → ∀ 𝑢 ( ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) → 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ) )
64 zornn0g ( ( { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∈ dom card ∧ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ≠ ∅ ∧ ∀ 𝑢 ( ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢 ) → 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ) ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ¬ 𝑠𝑤 )
65 25 53 63 64 syl3anc ( ( 𝜑𝑆𝑈 ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ¬ 𝑠𝑤 )
66 psseq1 ( 𝑣 = 𝑤 → ( 𝑣𝑈𝑤𝑈 ) )
67 eleq2 ( 𝑣 = 𝑤 → ( 𝐴𝑣𝐴𝑤 ) )
68 66 67 anbi12d ( 𝑣 = 𝑤 → ( ( 𝑣𝑈𝐴𝑣 ) ↔ ( 𝑤𝑈𝐴𝑤 ) ) )
69 68 ralrab ( ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ¬ 𝑠𝑤 ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) )
70 69 rexbii ( ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ¬ 𝑠𝑤 ↔ ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) )
71 65 70 sylib ( ( 𝜑𝑆𝑈 ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) )
72 71 ex ( 𝜑 → ( 𝑆𝑈 → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) )
73 psseq1 ( 𝑣 = 𝑠 → ( 𝑣𝑈𝑠𝑈 ) )
74 eleq2 ( 𝑣 = 𝑠 → ( 𝐴𝑣𝐴𝑠 ) )
75 73 74 anbi12d ( 𝑣 = 𝑠 → ( ( 𝑣𝑈𝐴𝑣 ) ↔ ( 𝑠𝑈𝐴𝑠 ) ) )
76 75 ralrab ( ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ↔ ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠𝑈𝐴𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ) )
77 14 76 sylibr ( 𝜑 → ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) )
78 r19.29 ( ( ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ∧ ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) )
79 75 elrab ( 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) )
80 ineq2 ( 𝑡 = 𝑣 → ( 𝑆𝑡 ) = ( 𝑆𝑣 ) )
81 80 eqeq1d ( 𝑡 = 𝑣 → ( ( 𝑆𝑡 ) = { 0 } ↔ ( 𝑆𝑣 ) = { 0 } ) )
82 oveq2 ( 𝑡 = 𝑣 → ( 𝑆 𝑡 ) = ( 𝑆 𝑣 ) )
83 82 eqeq1d ( 𝑡 = 𝑣 → ( ( 𝑆 𝑡 ) = 𝑠 ↔ ( 𝑆 𝑣 ) = 𝑠 ) )
84 81 83 anbi12d ( 𝑡 = 𝑣 → ( ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ↔ ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ) ) )
85 84 cbvrexvw ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ↔ ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ) )
86 simprrl ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) → 𝑠𝑈 )
87 86 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ) → 𝑠𝑈 )
88 simpr2 ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ) → ( 𝑆 𝑣 ) = 𝑠 )
89 88 psseq1d ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ) → ( ( 𝑆 𝑣 ) ⊊ 𝑈𝑠𝑈 ) )
90 87 89 mpbird ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ) → ( 𝑆 𝑣 ) ⊊ 𝑈 )
91 pssdif ( ( 𝑆 𝑣 ) ⊊ 𝑈 → ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ≠ ∅ )
92 n0 ( ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) )
93 91 92 sylib ( ( 𝑆 𝑣 ) ⊊ 𝑈 → ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) )
94 90 93 syl ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ) → ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) )
95 8 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → 𝑃 pGrp 𝐺 )
96 9 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → 𝐺 ∈ Abel )
97 10 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → 𝐵 ∈ Fin )
98 11 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → ( 𝑂𝐴 ) = 𝐸 )
99 12 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
100 13 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → 𝐴𝑈 )
101 simplr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → 𝑣 ∈ ( SubGrp ‘ 𝐺 ) )
102 simprl1 ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → ( 𝑆𝑣 ) = { 0 } )
103 90 adantrr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → ( 𝑆 𝑣 ) ⊊ 𝑈 )
104 103 pssssd ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → ( 𝑆 𝑣 ) ⊆ 𝑈 )
105 simprl3 ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) )
106 88 adantrr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → ( 𝑆 𝑣 ) = 𝑠 )
107 psseq1 ( ( 𝑆 𝑣 ) = 𝑠 → ( ( 𝑆 𝑣 ) ⊊ 𝑦𝑠𝑦 ) )
108 107 notbid ( ( 𝑆 𝑣 ) = 𝑠 → ( ¬ ( 𝑆 𝑣 ) ⊊ 𝑦 ↔ ¬ 𝑠𝑦 ) )
109 108 imbi2d ( ( 𝑆 𝑣 ) = 𝑠 → ( ( ( 𝑦𝑈𝐴𝑦 ) → ¬ ( 𝑆 𝑣 ) ⊊ 𝑦 ) ↔ ( ( 𝑦𝑈𝐴𝑦 ) → ¬ 𝑠𝑦 ) ) )
110 109 ralbidv ( ( 𝑆 𝑣 ) = 𝑠 → ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦𝑈𝐴𝑦 ) → ¬ ( 𝑆 𝑣 ) ⊊ 𝑦 ) ↔ ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦𝑈𝐴𝑦 ) → ¬ 𝑠𝑦 ) ) )
111 psseq1 ( 𝑦 = 𝑤 → ( 𝑦𝑈𝑤𝑈 ) )
112 eleq2 ( 𝑦 = 𝑤 → ( 𝐴𝑦𝐴𝑤 ) )
113 111 112 anbi12d ( 𝑦 = 𝑤 → ( ( 𝑦𝑈𝐴𝑦 ) ↔ ( 𝑤𝑈𝐴𝑤 ) ) )
114 psseq2 ( 𝑦 = 𝑤 → ( 𝑠𝑦𝑠𝑤 ) )
115 114 notbid ( 𝑦 = 𝑤 → ( ¬ 𝑠𝑦 ↔ ¬ 𝑠𝑤 ) )
116 113 115 imbi12d ( 𝑦 = 𝑤 → ( ( ( 𝑦𝑈𝐴𝑦 ) → ¬ 𝑠𝑦 ) ↔ ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) )
117 116 cbvralvw ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦𝑈𝐴𝑦 ) → ¬ 𝑠𝑦 ) ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) )
118 110 117 bitrdi ( ( 𝑆 𝑣 ) = 𝑠 → ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦𝑈𝐴𝑦 ) → ¬ ( 𝑆 𝑣 ) ⊊ 𝑦 ) ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) )
119 106 118 syl ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦𝑈𝐴𝑦 ) → ¬ ( 𝑆 𝑣 ) ⊊ 𝑦 ) ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) )
120 105 119 mpbird ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦𝑈𝐴𝑦 ) → ¬ ( 𝑆 𝑣 ) ⊊ 𝑦 ) )
121 simprr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) )
122 eqid ( .g𝐺 ) = ( .g𝐺 )
123 1 2 3 4 5 6 7 95 96 97 98 99 100 101 102 104 120 121 122 pgpfac1lem4 ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) )
124 123 expr ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ) → ( 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) )
125 124 exlimdv ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ) → ( ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 𝑣 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) )
126 94 125 mpd ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) )
127 126 3exp2 ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆𝑣 ) = { 0 } → ( ( 𝑆 𝑣 ) = 𝑠 → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) ) ) )
128 127 impd ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ) → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) ) )
129 128 rexlimdva ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) → ( ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑣 ) = { 0 } ∧ ( 𝑆 𝑣 ) = 𝑠 ) → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) ) )
130 85 129 syl5bi ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) → ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) ) )
131 130 impd ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠𝑈𝐴𝑠 ) ) ) → ( ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) )
132 79 131 sylan2b ( ( 𝜑𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ) → ( ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) )
133 132 rexlimdva ( 𝜑 → ( ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) )
134 78 133 syl5 ( 𝜑 → ( ( ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑠 ) ∧ ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) )
135 77 134 mpand ( 𝜑 → ( ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣𝑈𝐴𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤𝑈𝐴𝑤 ) → ¬ 𝑠𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) )
136 72 135 syld ( 𝜑 → ( 𝑆𝑈 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) )
137 6 0subg ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
138 27 137 syl ( 𝜑 → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
139 138 adantr ( ( 𝜑𝑆 = 𝑈 ) → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
140 6 subg0cl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0𝑆 )
141 36 140 syl ( 𝜑0𝑆 )
142 141 snssd ( 𝜑 → { 0 } ⊆ 𝑆 )
143 142 adantr ( ( 𝜑𝑆 = 𝑈 ) → { 0 } ⊆ 𝑆 )
144 sseqin2 ( { 0 } ⊆ 𝑆 ↔ ( 𝑆 ∩ { 0 } ) = { 0 } )
145 143 144 sylib ( ( 𝜑𝑆 = 𝑈 ) → ( 𝑆 ∩ { 0 } ) = { 0 } )
146 7 lsmss2 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ { 0 } ∈ ( SubGrp ‘ 𝐺 ) ∧ { 0 } ⊆ 𝑆 ) → ( 𝑆 { 0 } ) = 𝑆 )
147 36 138 142 146 syl3anc ( 𝜑 → ( 𝑆 { 0 } ) = 𝑆 )
148 147 eqeq1d ( 𝜑 → ( ( 𝑆 { 0 } ) = 𝑈𝑆 = 𝑈 ) )
149 148 biimpar ( ( 𝜑𝑆 = 𝑈 ) → ( 𝑆 { 0 } ) = 𝑈 )
150 ineq2 ( 𝑡 = { 0 } → ( 𝑆𝑡 ) = ( 𝑆 ∩ { 0 } ) )
151 150 eqeq1d ( 𝑡 = { 0 } → ( ( 𝑆𝑡 ) = { 0 } ↔ ( 𝑆 ∩ { 0 } ) = { 0 } ) )
152 oveq2 ( 𝑡 = { 0 } → ( 𝑆 𝑡 ) = ( 𝑆 { 0 } ) )
153 152 eqeq1d ( 𝑡 = { 0 } → ( ( 𝑆 𝑡 ) = 𝑈 ↔ ( 𝑆 { 0 } ) = 𝑈 ) )
154 151 153 anbi12d ( 𝑡 = { 0 } → ( ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ↔ ( ( 𝑆 ∩ { 0 } ) = { 0 } ∧ ( 𝑆 { 0 } ) = 𝑈 ) ) )
155 154 rspcev ( ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑆 ∩ { 0 } ) = { 0 } ∧ ( 𝑆 { 0 } ) = 𝑈 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) )
156 139 145 149 155 syl12anc ( ( 𝜑𝑆 = 𝑈 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) )
157 156 ex ( 𝜑 → ( 𝑆 = 𝑈 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ) )
158 1 mrcsscl ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ { 𝐴 } ⊆ 𝑈𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐾 ‘ { 𝐴 } ) ⊆ 𝑈 )
159 30 39 12 158 syl3anc ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ⊆ 𝑈 )
160 2 159 eqsstrid ( 𝜑𝑆𝑈 )
161 sspss ( 𝑆𝑈 ↔ ( 𝑆𝑈𝑆 = 𝑈 ) )
162 160 161 sylib ( 𝜑 → ( 𝑆𝑈𝑆 = 𝑈 ) )
163 136 157 162 mpjaod ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) )