| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ghmqusnsg.j | . . 3
⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪
(𝐹 “ 𝑞)) | 
| 2 |  | imaeq2 6074 | . . . 4
⊢ (𝑞 = [𝑋](𝐺 ~QG 𝑁) → (𝐹 “ 𝑞) = (𝐹 “ [𝑋](𝐺 ~QG 𝑁))) | 
| 3 | 2 | unieqd 4920 | . . 3
⊢ (𝑞 = [𝑋](𝐺 ~QG 𝑁) → ∪ (𝐹 “ 𝑞) = ∪ (𝐹 “ [𝑋](𝐺 ~QG 𝑁))) | 
| 4 |  | ghmqusnsglem1.x | . . . . 5
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺)) | 
| 5 |  | ovex 7464 | . . . . . 6
⊢ (𝐺 ~QG 𝑁) ∈ V | 
| 6 | 5 | ecelqsi 8813 | . . . . 5
⊢ (𝑋 ∈ (Base‘𝐺) → [𝑋](𝐺 ~QG 𝑁) ∈ ((Base‘𝐺) / (𝐺 ~QG 𝑁))) | 
| 7 | 4, 6 | syl 17 | . . . 4
⊢ (𝜑 → [𝑋](𝐺 ~QG 𝑁) ∈ ((Base‘𝐺) / (𝐺 ~QG 𝑁))) | 
| 8 |  | ghmqusnsg.q | . . . . . 6
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) | 
| 9 | 8 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))) | 
| 10 |  | eqidd 2738 | . . . . 5
⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐺)) | 
| 11 |  | ovexd 7466 | . . . . 5
⊢ (𝜑 → (𝐺 ~QG 𝑁) ∈ V) | 
| 12 |  | ghmqusnsg.f | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | 
| 13 |  | ghmgrp1 19236 | . . . . . 6
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp) | 
| 14 | 12, 13 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 15 | 9, 10, 11, 14 | qusbas 17590 | . . . 4
⊢ (𝜑 → ((Base‘𝐺) / (𝐺 ~QG 𝑁)) = (Base‘𝑄)) | 
| 16 | 7, 15 | eleqtrd 2843 | . . 3
⊢ (𝜑 → [𝑋](𝐺 ~QG 𝑁) ∈ (Base‘𝑄)) | 
| 17 | 12 | imaexd 7938 | . . . 4
⊢ (𝜑 → (𝐹 “ [𝑋](𝐺 ~QG 𝑁)) ∈ V) | 
| 18 | 17 | uniexd 7762 | . . 3
⊢ (𝜑 → ∪ (𝐹
“ [𝑋](𝐺 ~QG 𝑁)) ∈ V) | 
| 19 | 1, 3, 16, 18 | fvmptd3 7039 | . 2
⊢ (𝜑 → (𝐽‘[𝑋](𝐺 ~QG 𝑁)) = ∪ (𝐹 “ [𝑋](𝐺 ~QG 𝑁))) | 
| 20 |  | eqid 2737 | . . . . . . . . . 10
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 21 |  | eqid 2737 | . . . . . . . . . 10
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 22 | 20, 21 | ghmf 19238 | . . . . . . . . 9
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) | 
| 23 | 12, 22 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) | 
| 24 | 23 | ffnd 6737 | . . . . . . 7
⊢ (𝜑 → 𝐹 Fn (Base‘𝐺)) | 
| 25 |  | ghmqusnsg.1 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) | 
| 26 |  | nsgsubg 19176 | . . . . . . . . 9
⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → 𝑁 ∈ (SubGrp‘𝐺)) | 
| 27 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝐺 ~QG 𝑁) = (𝐺 ~QG 𝑁) | 
| 28 | 20, 27 | eqger 19196 | . . . . . . . . 9
⊢ (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝑁) Er (Base‘𝐺)) | 
| 29 | 25, 26, 28 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → (𝐺 ~QG 𝑁) Er (Base‘𝐺)) | 
| 30 | 29 | ecss 8793 | . . . . . . 7
⊢ (𝜑 → [𝑋](𝐺 ~QG 𝑁) ⊆ (Base‘𝐺)) | 
| 31 | 24, 30 | fvelimabd 6982 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐹 “ [𝑋](𝐺 ~QG 𝑁)) ↔ ∃𝑧 ∈ [ 𝑋](𝐺 ~QG 𝑁)(𝐹‘𝑧) = 𝑦)) | 
| 32 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) ∧ (𝐹‘𝑧) = 𝑦) → (𝐹‘𝑧) = 𝑦) | 
| 33 | 12 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | 
| 34 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 35 | 33, 13 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝐺 ∈ Grp) | 
| 36 | 4 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝑋 ∈ (Base‘𝐺)) | 
| 37 | 20, 34, 35, 36 | grpinvcld 19006 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → ((invg‘𝐺)‘𝑋) ∈ (Base‘𝐺)) | 
| 38 | 30 | sselda 3983 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝑧 ∈ (Base‘𝐺)) | 
| 39 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 40 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(+g‘𝐻) = (+g‘𝐻) | 
| 41 | 20, 39, 40 | ghmlin 19239 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ ((invg‘𝐺)‘𝑋) ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝐹‘(((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧)) = ((𝐹‘((invg‘𝐺)‘𝑋))(+g‘𝐻)(𝐹‘𝑧))) | 
| 42 | 33, 37, 38, 41 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → (𝐹‘(((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧)) = ((𝐹‘((invg‘𝐺)‘𝑋))(+g‘𝐻)(𝐹‘𝑧))) | 
| 43 | 24 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝐹 Fn (Base‘𝐺)) | 
| 44 |  | ghmqusnsg.n | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ⊆ 𝐾) | 
| 45 |  | ghmqusnsg.k | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐾 = (◡𝐹 “ { 0 }) | 
| 46 | 44, 45 | sseqtrdi 4024 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ⊆ (◡𝐹 “ { 0 })) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝑁 ⊆ (◡𝐹 “ { 0 })) | 
| 48 | 20 | subgss 19145 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 ⊆ (Base‘𝐺)) | 
| 49 | 25, 26, 48 | 3syl 18 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ⊆ (Base‘𝐺)) | 
| 50 | 49 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝑁 ⊆ (Base‘𝐺)) | 
| 51 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑧 ∈ V | 
| 52 |  | elecg 8789 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ V ∧ 𝑋 ∈ (Base‘𝐺)) → (𝑧 ∈ [𝑋](𝐺 ~QG 𝑁) ↔ 𝑋(𝐺 ~QG 𝑁)𝑧)) | 
| 53 | 51, 52 | mpan 690 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 ∈ (Base‘𝐺) → (𝑧 ∈ [𝑋](𝐺 ~QG 𝑁) ↔ 𝑋(𝐺 ~QG 𝑁)𝑧)) | 
| 54 | 53 | biimpa 476 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ (Base‘𝐺) ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝑋(𝐺 ~QG 𝑁)𝑧) | 
| 55 | 4, 54 | sylan 580 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝑋(𝐺 ~QG 𝑁)𝑧) | 
| 56 | 20, 34, 39, 27 | eqgval 19195 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ⊆ (Base‘𝐺)) → (𝑋(𝐺 ~QG 𝑁)𝑧 ↔ (𝑋 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ 𝑁))) | 
| 57 | 56 | biimpa 476 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ⊆ (Base‘𝐺)) ∧ 𝑋(𝐺 ~QG 𝑁)𝑧) → (𝑋 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ 𝑁)) | 
| 58 | 57 | simp3d 1145 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ⊆ (Base‘𝐺)) ∧ 𝑋(𝐺 ~QG 𝑁)𝑧) → (((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ 𝑁) | 
| 59 | 35, 50, 55, 58 | syl21anc 838 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → (((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ 𝑁) | 
| 60 | 47, 59 | sseldd 3984 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → (((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ (◡𝐹 “ { 0 })) | 
| 61 |  | fniniseg 7080 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn (Base‘𝐺) →
((((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ (◡𝐹 “ { 0 }) ↔
((((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ (Base‘𝐺) ∧ (𝐹‘(((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧)) = 0 ))) | 
| 62 | 61 | biimpa 476 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn (Base‘𝐺) ∧
(((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ (◡𝐹 “ { 0 })) →
((((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ (Base‘𝐺) ∧ (𝐹‘(((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧)) = 0 )) | 
| 63 | 43, 60, 62 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → ((((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧) ∈ (Base‘𝐺) ∧ (𝐹‘(((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧)) = 0 )) | 
| 64 | 63 | simprd 495 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → (𝐹‘(((invg‘𝐺)‘𝑋)(+g‘𝐺)𝑧)) = 0 ) | 
| 65 | 42, 64 | eqtr3d 2779 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → ((𝐹‘((invg‘𝐺)‘𝑋))(+g‘𝐻)(𝐹‘𝑧)) = 0 ) | 
| 66 | 65 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → ((𝐹‘𝑋)(+g‘𝐻)((𝐹‘((invg‘𝐺)‘𝑋))(+g‘𝐻)(𝐹‘𝑧))) = ((𝐹‘𝑋)(+g‘𝐻) 0 )) | 
| 67 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(invg‘𝐻) = (invg‘𝐻) | 
| 68 | 20, 34, 67 | ghminv 19241 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑋 ∈ (Base‘𝐺)) → (𝐹‘((invg‘𝐺)‘𝑋)) = ((invg‘𝐻)‘(𝐹‘𝑋))) | 
| 69 | 33, 36, 68 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → (𝐹‘((invg‘𝐺)‘𝑋)) = ((invg‘𝐻)‘(𝐹‘𝑋))) | 
| 70 | 69 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → ((𝐹‘((invg‘𝐺)‘𝑋))(+g‘𝐻)(𝐹‘𝑧)) = (((invg‘𝐻)‘(𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑧))) | 
| 71 | 70 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → ((𝐹‘𝑋)(+g‘𝐻)((𝐹‘((invg‘𝐺)‘𝑋))(+g‘𝐻)(𝐹‘𝑧))) = ((𝐹‘𝑋)(+g‘𝐻)(((invg‘𝐻)‘(𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑧)))) | 
| 72 |  | ghmgrp2 19237 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp) | 
| 73 | 33, 72 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝐻 ∈ Grp) | 
| 74 | 33, 22 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) | 
| 75 | 74, 36 | ffvelcdmd 7105 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → (𝐹‘𝑋) ∈ (Base‘𝐻)) | 
| 76 | 74, 38 | ffvelcdmd 7105 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → (𝐹‘𝑧) ∈ (Base‘𝐻)) | 
| 77 | 21, 40, 67 | grpasscan1 19019 | . . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ Grp ∧ (𝐹‘𝑋) ∈ (Base‘𝐻) ∧ (𝐹‘𝑧) ∈ (Base‘𝐻)) → ((𝐹‘𝑋)(+g‘𝐻)(((invg‘𝐻)‘(𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑧))) = (𝐹‘𝑧)) | 
| 78 | 73, 75, 76, 77 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → ((𝐹‘𝑋)(+g‘𝐻)(((invg‘𝐻)‘(𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑧))) = (𝐹‘𝑧)) | 
| 79 | 71, 78 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → ((𝐹‘𝑋)(+g‘𝐻)((𝐹‘((invg‘𝐺)‘𝑋))(+g‘𝐻)(𝐹‘𝑧))) = (𝐹‘𝑧)) | 
| 80 |  | ghmqusnsg.0 | . . . . . . . . . . . . 13
⊢  0 =
(0g‘𝐻) | 
| 81 | 21, 40, 80, 73, 75 | grpridd 18988 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → ((𝐹‘𝑋)(+g‘𝐻) 0 ) = (𝐹‘𝑋)) | 
| 82 | 66, 79, 81 | 3eqtr3d 2785 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) → (𝐹‘𝑧) = (𝐹‘𝑋)) | 
| 83 | 82 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) ∧ (𝐹‘𝑧) = 𝑦) → (𝐹‘𝑧) = (𝐹‘𝑋)) | 
| 84 | 32, 83 | eqtr3d 2779 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ [𝑋](𝐺 ~QG 𝑁)) ∧ (𝐹‘𝑧) = 𝑦) → 𝑦 = (𝐹‘𝑋)) | 
| 85 | 84 | r19.29an 3158 | . . . . . . . 8
⊢ ((𝜑 ∧ ∃𝑧 ∈ [ 𝑋](𝐺 ~QG 𝑁)(𝐹‘𝑧) = 𝑦) → 𝑦 = (𝐹‘𝑋)) | 
| 86 |  | fveqeq2 6915 | . . . . . . . . 9
⊢ (𝑧 = 𝑋 → ((𝐹‘𝑧) = 𝑦 ↔ (𝐹‘𝑋) = 𝑦)) | 
| 87 |  | ecref 8790 | . . . . . . . . . . 11
⊢ (((𝐺 ~QG 𝑁) Er (Base‘𝐺) ∧ 𝑋 ∈ (Base‘𝐺)) → 𝑋 ∈ [𝑋](𝐺 ~QG 𝑁)) | 
| 88 | 29, 4, 87 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ [𝑋](𝐺 ~QG 𝑁)) | 
| 89 | 88 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑋)) → 𝑋 ∈ [𝑋](𝐺 ~QG 𝑁)) | 
| 90 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑋)) → 𝑦 = (𝐹‘𝑋)) | 
| 91 | 90 | eqcomd 2743 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑋)) → (𝐹‘𝑋) = 𝑦) | 
| 92 | 86, 89, 91 | rspcedvdw 3625 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑋)) → ∃𝑧 ∈ [ 𝑋](𝐺 ~QG 𝑁)(𝐹‘𝑧) = 𝑦) | 
| 93 | 85, 92 | impbida 801 | . . . . . . 7
⊢ (𝜑 → (∃𝑧 ∈ [ 𝑋](𝐺 ~QG 𝑁)(𝐹‘𝑧) = 𝑦 ↔ 𝑦 = (𝐹‘𝑋))) | 
| 94 |  | velsn 4642 | . . . . . . 7
⊢ (𝑦 ∈ {(𝐹‘𝑋)} ↔ 𝑦 = (𝐹‘𝑋)) | 
| 95 | 93, 94 | bitr4di 289 | . . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ [ 𝑋](𝐺 ~QG 𝑁)(𝐹‘𝑧) = 𝑦 ↔ 𝑦 ∈ {(𝐹‘𝑋)})) | 
| 96 | 31, 95 | bitrd 279 | . . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐹 “ [𝑋](𝐺 ~QG 𝑁)) ↔ 𝑦 ∈ {(𝐹‘𝑋)})) | 
| 97 | 96 | eqrdv 2735 | . . . 4
⊢ (𝜑 → (𝐹 “ [𝑋](𝐺 ~QG 𝑁)) = {(𝐹‘𝑋)}) | 
| 98 | 97 | unieqd 4920 | . . 3
⊢ (𝜑 → ∪ (𝐹
“ [𝑋](𝐺 ~QG 𝑁)) = ∪ {(𝐹‘𝑋)}) | 
| 99 |  | fvex 6919 | . . . 4
⊢ (𝐹‘𝑋) ∈ V | 
| 100 | 99 | unisn 4926 | . . 3
⊢ ∪ {(𝐹‘𝑋)} = (𝐹‘𝑋) | 
| 101 | 98, 100 | eqtrdi 2793 | . 2
⊢ (𝜑 → ∪ (𝐹
“ [𝑋](𝐺 ~QG 𝑁)) = (𝐹‘𝑋)) | 
| 102 | 19, 101 | eqtrd 2777 | 1
⊢ (𝜑 → (𝐽‘[𝑋](𝐺 ~QG 𝑁)) = (𝐹‘𝑋)) |