Metamath Proof Explorer

Theorem nsgmgc

Description: There is a monotone Galois connection between the lattice of subgroups of a group G containing a normal subgroup N and the lattice of subgroups of the quotient group G / N . This is sometimes called the lattice theorem. (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypotheses nsgmgc.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
nsgmgc.s ⊢ 𝑆 = { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝑁 ⊆ ℎ }
nsgmgc.t ⊢ 𝑇 = ( SubGrp ‘ 𝑄 )
nsgmgc.j ⊢ 𝐽 = ( 𝑉 MGalConn 𝑊 )
nsgmgc.v ⊢ 𝑉 = ( toInc ‘ 𝑆 )
nsgmgc.w ⊢ 𝑊 = ( toInc ‘ 𝑇 )
nsgmgc.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
nsgmgc.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
nsgmgc.e ⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
nsgmgc.f ⊢ 𝐹 = ( 𝑓 ∈ 𝑇 ↦ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
nsgmgc.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
Assertion nsgmgc ( 𝜑 → 𝐸 𝐽 𝐹 )

Proof

Step Hyp Ref Expression
1 nsgmgc.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 nsgmgc.s ⊢ 𝑆 = { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝑁 ⊆ ℎ }
3 nsgmgc.t ⊢ 𝑇 = ( SubGrp ‘ 𝑄 )
4 nsgmgc.j ⊢ 𝐽 = ( 𝑉 MGalConn 𝑊 )
5 nsgmgc.v ⊢ 𝑉 = ( toInc ‘ 𝑆 )
6 nsgmgc.w ⊢ 𝑊 = ( toInc ‘ 𝑇 )
7 nsgmgc.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
8 nsgmgc.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
9 nsgmgc.e ⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
10 nsgmgc.f ⊢ 𝐹 = ( 𝑓 ∈ 𝑇 ↦ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
11 nsgmgc.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
12 nfv ⊢ Ⅎ ℎ 𝜑
13 vex ⊢ ℎ ∈ V
14 13 mptex ⊢ ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ V
15 14 rnex ⊢ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ V
16 15 a1i ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ V )
17 12 16 9 fnmptd ⊢ ( 𝜑 → 𝐸 Fn 𝑆 )
18 mpteq1 ⊢ ( ℎ = 𝑘 → ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑥 ∈ 𝑘 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
19 18 rneqd ⊢ ( ℎ = 𝑘 → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ran ( 𝑥 ∈ 𝑘 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
20 19 cbvmptv ⊢ ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) = ( 𝑘 ∈ 𝑆 ↦ ran ( 𝑥 ∈ 𝑘 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
21 9 20 eqtri ⊢ 𝐸 = ( 𝑘 ∈ 𝑆 ↦ ran ( 𝑥 ∈ 𝑘 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
22 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
23 11 adantr ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
24 simpr ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ℎ ∈ 𝑆 )
25 2 ssrab3 ⊢ 𝑆 ⊆ ( SubGrp ‘ 𝐺 )
26 25 a1i ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
27 1 7 8 21 22 23 24 26 qusima ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ( 𝐸 ‘ ℎ ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) “ ℎ ) )
28 1 7 22 qusghm ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) ∈ ( 𝐺 GrpHom 𝑄 ) )
29 23 28 syl ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) ∈ ( 𝐺 GrpHom 𝑄 ) )
30 25 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
31 30 sselda ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ℎ ∈ ( SubGrp ‘ 𝐺 ) )
32 ghmima ⊢ ( ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) ∈ ( 𝐺 GrpHom 𝑄 ) ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) “ ℎ ) ∈ ( SubGrp ‘ 𝑄 ) )
33 29 31 32 syl2anc ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) “ ℎ ) ∈ ( SubGrp ‘ 𝑄 ) )
34 27 33 eqeltrd ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ( 𝐸 ‘ ℎ ) ∈ ( SubGrp ‘ 𝑄 ) )
35 34 3 eleqtrrdi ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ( 𝐸 ‘ ℎ ) ∈ 𝑇 )
36 35 ralrimiva ⊢ ( 𝜑 → ∀ ℎ ∈ 𝑆 ( 𝐸 ‘ ℎ ) ∈ 𝑇 )
37 ffnfv ⊢ ( 𝐸 : 𝑆 ⟶ 𝑇 ↔ ( 𝐸 Fn 𝑆 ∧ ∀ ℎ ∈ 𝑆 ( 𝐸 ‘ ℎ ) ∈ 𝑇 ) )
38 17 36 37 sylanbrc ⊢ ( 𝜑 → 𝐸 : 𝑆 ⟶ 𝑇 )
39 sseq2 ⊢ ( ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } → ( 𝑁 ⊆ ℎ ↔ 𝑁 ⊆ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) )
40 11 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑓 ∈ 𝑇 )
42 41 3 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑓 ∈ ( SubGrp ‘ 𝑄 ) )
43 1 7 8 40 42 nsgmgclem ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ ( SubGrp ‘ 𝐺 ) )
44 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
45 11 44 syl ⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
46 1 subgss ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 ⊆ 𝐵 )
47 45 46 syl ⊢ ( 𝜑 → 𝑁 ⊆ 𝐵 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ⊆ 𝐵 )
49 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
50 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
51 8 grplsmid ⊢ ( ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑎 } ⊕ 𝑁 ) = 𝑁 )
52 49 50 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑎 } ⊕ 𝑁 ) = 𝑁 )
53 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
54 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑓 ∈ ( SubGrp ‘ 𝑄 ) )
55 7 nsgqus0 ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ∈ 𝑓 )
56 53 54 55 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ 𝑓 )
57 52 56 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 )
58 48 57 ssrabdv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ⊆ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
59 39 43 58 elrabd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝑁 ⊆ ℎ } )
60 59 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ 𝑆 )
61 60 10 fmptd ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ 𝑆 )
62 38 61 jca ⊢ ( 𝜑 → ( 𝐸 : 𝑆 ⟶ 𝑇 ∧ 𝐹 : 𝑇 ⟶ 𝑆 ) )
63 1 subgss ⊢ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) → ℎ ⊆ 𝐵 )
64 31 63 syl ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ℎ ⊆ 𝐵 )
65 64 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) → ℎ ⊆ 𝐵 )
66 9 fvmpt2 ⊢ ( ( ℎ ∈ 𝑆 ∧ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ V ) → ( 𝐸 ‘ ℎ ) = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
67 24 15 66 sylancl ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ( 𝐸 ‘ ℎ ) = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
68 67 ad5ant12 ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) → ( 𝐸 ‘ ℎ ) = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
69 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) → ( 𝐸 ‘ ℎ ) ⊆ 𝑓 )
70 68 69 eqsstrrd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ⊆ 𝑓 )
71 eqid ⊢ ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
72 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) → 𝑎 ∈ ℎ )
73 sneq ⊢ ( 𝑥 = 𝑎 → { 𝑥 } = { 𝑎 } )
74 73 oveq1d ⊢ ( 𝑥 = 𝑎 → ( { 𝑥 } ⊕ 𝑁 ) = ( { 𝑎 } ⊕ 𝑁 ) )
75 74 eqeq2d ⊢ ( 𝑥 = 𝑎 → ( ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ↔ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑎 } ⊕ 𝑁 ) ) )
76 75 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) ∧ 𝑥 = 𝑎 ) → ( ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ↔ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑎 } ⊕ 𝑁 ) ) )
77 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) → ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑎 } ⊕ 𝑁 ) )
78 72 76 77 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) → ∃ 𝑥 ∈ ℎ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
79 ovexd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) → ( { 𝑎 } ⊕ 𝑁 ) ∈ V )
80 71 78 79 elrnmptd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) → ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
81 70 80 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) ∧ 𝑎 ∈ ℎ ) → ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 )
82 65 81 ssrabdv ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) → ℎ ⊆ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
83 simpr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) → 𝑓 ∈ 𝑇 )
84 1 fvexi ⊢ 𝐵 ∈ V
85 84 rabex ⊢ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ V
86 10 fvmpt2 ⊢ ( ( 𝑓 ∈ 𝑇 ∧ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ V ) → ( 𝐹 ‘ 𝑓 ) = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
87 83 85 86 sylancl ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑓 ) = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
88 87 adantr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) → ( 𝐹 ‘ 𝑓 ) = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
89 82 88 sseqtrrd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) → ℎ ⊆ ( 𝐹 ‘ 𝑓 ) )
90 67 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) → ( 𝐸 ‘ ℎ ) = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
91 simpr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) → ℎ ⊆ ( 𝐹 ‘ 𝑓 ) )
92 91 sselda ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℎ ) → 𝑥 ∈ ( 𝐹 ‘ 𝑓 ) )
93 87 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℎ ) → ( 𝐹 ‘ 𝑓 ) = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
94 92 93 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℎ ) → 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
95 sneq ⊢ ( 𝑎 = 𝑥 → { 𝑎 } = { 𝑥 } )
96 95 oveq1d ⊢ ( 𝑎 = 𝑥 → ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
97 96 eleq1d ⊢ ( 𝑎 = 𝑥 → ( ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 ↔ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) )
98 97 elrab ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↔ ( 𝑥 ∈ 𝐵 ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) )
99 98 simprbi ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } → ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 )
100 94 99 syl ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℎ ) → ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 )
101 100 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) → ∀ 𝑥 ∈ ℎ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 )
102 71 rnmptss ⊢ ( ∀ 𝑥 ∈ ℎ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ⊆ 𝑓 )
103 101 102 syl ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ⊆ 𝑓 )
104 90 103 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) → ( 𝐸 ‘ ℎ ) ⊆ 𝑓 )
105 89 104 impbida ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ↔ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) )
106 3 fvexi ⊢ 𝑇 ∈ V
107 eqid ⊢ ( le ‘ 𝑊 ) = ( le ‘ 𝑊 )
108 6 107 ipole ⊢ ( ( 𝑇 ∈ V ∧ ( 𝐸 ‘ ℎ ) ∈ 𝑇 ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝐸 ‘ ℎ ) ( le ‘ 𝑊 ) 𝑓 ↔ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) )
109 106 35 83 108 mp3an2ani ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝐸 ‘ ℎ ) ( le ‘ 𝑊 ) 𝑓 ↔ ( 𝐸 ‘ ℎ ) ⊆ 𝑓 ) )
110 fvex ⊢ ( SubGrp ‘ 𝐺 ) ∈ V
111 2 110 rabex2 ⊢ 𝑆 ∈ V
112 61 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑓 ) ∈ 𝑆 )
113 112 adantlr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑓 ) ∈ 𝑆 )
114 eqid ⊢ ( le ‘ 𝑉 ) = ( le ‘ 𝑉 )
115 5 114 ipole ⊢ ( ( 𝑆 ∈ V ∧ ℎ ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑓 ) ∈ 𝑆 ) → ( ℎ ( le ‘ 𝑉 ) ( 𝐹 ‘ 𝑓 ) ↔ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) )
116 111 24 113 115 mp3an2ani ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) → ( ℎ ( le ‘ 𝑉 ) ( 𝐹 ‘ 𝑓 ) ↔ ℎ ⊆ ( 𝐹 ‘ 𝑓 ) ) )
117 105 109 116 3bitr4d ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝐸 ‘ ℎ ) ( le ‘ 𝑊 ) 𝑓 ↔ ℎ ( le ‘ 𝑉 ) ( 𝐹 ‘ 𝑓 ) ) )
118 117 anasss ⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝑆 ∧ 𝑓 ∈ 𝑇 ) ) → ( ( 𝐸 ‘ ℎ ) ( le ‘ 𝑊 ) 𝑓 ↔ ℎ ( le ‘ 𝑉 ) ( 𝐹 ‘ 𝑓 ) ) )
119 118 ralrimivva ⊢ ( 𝜑 → ∀ ℎ ∈ 𝑆 ∀ 𝑓 ∈ 𝑇 ( ( 𝐸 ‘ ℎ ) ( le ‘ 𝑊 ) 𝑓 ↔ ℎ ( le ‘ 𝑉 ) ( 𝐹 ‘ 𝑓 ) ) )
120 5 ipobas ⊢ ( 𝑆 ∈ V → 𝑆 = ( Base ‘ 𝑉 ) )
121 111 120 ax-mp ⊢ 𝑆 = ( Base ‘ 𝑉 )
122 6 ipobas ⊢ ( 𝑇 ∈ V → 𝑇 = ( Base ‘ 𝑊 ) )
123 106 122 ax-mp ⊢ 𝑇 = ( Base ‘ 𝑊 )
124 5 ipopos ⊢ 𝑉 ∈ Poset
125 posprs ⊢ ( 𝑉 ∈ Poset → 𝑉 ∈ Proset )
126 124 125 mp1i ⊢ ( 𝜑 → 𝑉 ∈ Proset )
127 6 ipopos ⊢ 𝑊 ∈ Poset
128 posprs ⊢ ( 𝑊 ∈ Poset → 𝑊 ∈ Proset )
129 127 128 mp1i ⊢ ( 𝜑 → 𝑊 ∈ Proset )
130 121 123 114 107 4 126 129 mgcval ⊢ ( 𝜑 → ( 𝐸 𝐽 𝐹 ↔ ( ( 𝐸 : 𝑆 ⟶ 𝑇 ∧ 𝐹 : 𝑇 ⟶ 𝑆 ) ∧ ∀ ℎ ∈ 𝑆 ∀ 𝑓 ∈ 𝑇 ( ( 𝐸 ‘ ℎ ) ( le ‘ 𝑊 ) 𝑓 ↔ ℎ ( le ‘ 𝑉 ) ( 𝐹 ‘ 𝑓 ) ) ) ) )
131 62 119 130 mpbir2and ⊢ ( 𝜑 → 𝐸 𝐽 𝐹 )