Metamath Proof Explorer

Theorem symgfixfolem1

Description: Lemma 1 for symgfixfo . (Contributed by AV, 7-Jan-2019)

Ref Expression
Hypotheses symgfixf.p ⊢ P = Base SymGrp ⁡ N
symgfixf.q ⊢ Q = q ∈ P | q ⁡ K = K
symgfixf.s ⊢ S = Base SymGrp ⁡ N ∖ K
symgfixf.h ⊢ H = q ∈ Q ⟼ q ↾ N ∖ K
symgfixfo.e ⊢ E = x ∈ N ⟼ if x = K K Z ⁡ x
Assertion symgfixfolem1 ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E ∈ Q

Proof

Step Hyp Ref Expression
1 symgfixf.p ⊢ P = Base SymGrp ⁡ N
2 symgfixf.q ⊢ Q = q ∈ P | q ⁡ K = K
3 symgfixf.s ⊢ S = Base SymGrp ⁡ N ∖ K
4 symgfixf.h ⊢ H = q ∈ Q ⟼ q ↾ N ∖ K
5 symgfixfo.e ⊢ E = x ∈ N ⟼ if x = K K Z ⁡ x
6 3 5 symgextf1o ⊢ K ∈ N ∧ Z ∈ S → E : N ⟶ 1-1 onto N
7 6 3adant1 ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E : N ⟶ 1-1 onto N
8 iftrue ⊢ x = K → if x = K K Z ⁡ x = K
9 simp2 ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → K ∈ N
10 5 8 9 9 fvmptd3 ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E ⁡ K = K
11 mptexg ⊢ N ∈ V → x ∈ N ⟼ if x = K K Z ⁡ x ∈ V
12 11 3ad2ant1 ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → x ∈ N ⟼ if x = K K Z ⁡ x ∈ V
13 5 12 eqeltrid ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E ∈ V
14 1 2 symgfixelq ⊢ E ∈ V → E ∈ Q ↔ E : N ⟶ 1-1 onto N ∧ E ⁡ K = K
15 13 14 syl ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E ∈ Q ↔ E : N ⟶ 1-1 onto N ∧ E ⁡ K = K
16 7 10 15 mpbir2and ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E ∈ Q