Theorem pmtrdifellem4

Description: Lemma 4 for pmtrdifel . (Contributed by AV, 28-Jan-2019)

	Ref	Expression
Hypotheses	pmtrdifel.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
	pmtrdifel.r	⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
	pmtrdifel.0	⊢ 𝑆 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) )
Assertion	pmtrdifellem4	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑆 ‘ 𝐾 ) = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		pmtrdifel.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
2		pmtrdifel.r	⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
3		pmtrdifel.0	⊢ 𝑆 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) )
4	1 2 3	pmtrdifellem1	⊢ ( 𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅 )
5		eqid	⊢ ( pmTrsp ‘ 𝑁 ) = ( pmTrsp ‘ 𝑁 )
6		eqid	⊢ dom ( 𝑆 ∖ I ) = dom ( 𝑆 ∖ I )
7	5 2 6	pmtrffv	⊢ ( ( 𝑆 ∈ 𝑅 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑆 ‘ 𝐾 ) = if ( 𝐾 ∈ dom ( 𝑆 ∖ I ) , ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝐾 } ) , 𝐾 ) )
8	4 7	sylan	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑆 ‘ 𝐾 ) = if ( 𝐾 ∈ dom ( 𝑆 ∖ I ) , ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝐾 } ) , 𝐾 ) )
9		eqid	⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
10		eqid	⊢ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
11	1 9 10	symgtrf	⊢ 𝑇 ⊆ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
12	11	sseli	⊢ ( 𝑄 ∈ 𝑇 → 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) )
13	9 10	symgbasf	⊢ ( 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) → 𝑄 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) )
14		ffn	⊢ ( 𝑄 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) → 𝑄 Fn ( 𝑁 ∖ { 𝐾 } ) )
15		fndifnfp	⊢ ( 𝑄 Fn ( 𝑁 ∖ { 𝐾 } ) → dom ( 𝑄 ∖ I ) = { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } )
16		ssrab2	⊢ { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } ⊆ ( 𝑁 ∖ { 𝐾 } )
17		ssel2	⊢ ( ( { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } ⊆ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐾 ∈ { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } ) → 𝐾 ∈ ( 𝑁 ∖ { 𝐾 } ) )
18		eldif	⊢ ( 𝐾 ∈ ( 𝑁 ∖ { 𝐾 } ) ↔ ( 𝐾 ∈ 𝑁 ∧ ¬ 𝐾 ∈ { 𝐾 } ) )
19		elsng	⊢ ( 𝐾 ∈ 𝑁 → ( 𝐾 ∈ { 𝐾 } ↔ 𝐾 = 𝐾 ) )
20	19	notbid	⊢ ( 𝐾 ∈ 𝑁 → ( ¬ 𝐾 ∈ { 𝐾 } ↔ ¬ 𝐾 = 𝐾 ) )
21		eqid	⊢ 𝐾 = 𝐾
22	21	pm2.24i	⊢ ( ¬ 𝐾 = 𝐾 → ¬ 𝐾 ∈ 𝑁 )
23	20 22	syl6bi	⊢ ( 𝐾 ∈ 𝑁 → ( ¬ 𝐾 ∈ { 𝐾 } → ¬ 𝐾 ∈ 𝑁 ) )
24	23	imp	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ¬ 𝐾 ∈ { 𝐾 } ) → ¬ 𝐾 ∈ 𝑁 )
25	18 24	sylbi	⊢ ( 𝐾 ∈ ( 𝑁 ∖ { 𝐾 } ) → ¬ 𝐾 ∈ 𝑁 )
26	17 25	syl	⊢ ( ( { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } ⊆ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐾 ∈ { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } ) → ¬ 𝐾 ∈ 𝑁 )
27	16 26	mpan	⊢ ( 𝐾 ∈ { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } → ¬ 𝐾 ∈ 𝑁 )
28	27	con2i	⊢ ( 𝐾 ∈ 𝑁 → ¬ 𝐾 ∈ { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } )
29		eleq2	⊢ ( dom ( 𝑄 ∖ I ) = { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } → ( 𝐾 ∈ dom ( 𝑄 ∖ I ) ↔ 𝐾 ∈ { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } ) )
30	29	notbid	⊢ ( dom ( 𝑄 ∖ I ) = { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } → ( ¬ 𝐾 ∈ dom ( 𝑄 ∖ I ) ↔ ¬ 𝐾 ∈ { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } ) )
31	28 30	syl5ibr	⊢ ( dom ( 𝑄 ∖ I ) = { 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ∣ ( 𝑄 ‘ 𝑥 ) ≠ 𝑥 } → ( 𝐾 ∈ 𝑁 → ¬ 𝐾 ∈ dom ( 𝑄 ∖ I ) ) )
32	14 15 31	3syl	⊢ ( 𝑄 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐾 ∈ 𝑁 → ¬ 𝐾 ∈ dom ( 𝑄 ∖ I ) ) )
33	12 13 32	3syl	⊢ ( 𝑄 ∈ 𝑇 → ( 𝐾 ∈ 𝑁 → ¬ 𝐾 ∈ dom ( 𝑄 ∖ I ) ) )
34	33	imp	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ¬ 𝐾 ∈ dom ( 𝑄 ∖ I ) )
35	1 2 3	pmtrdifellem2	⊢ ( 𝑄 ∈ 𝑇 → dom ( 𝑆 ∖ I ) = dom ( 𝑄 ∖ I ) )
36	35	eleq2d	⊢ ( 𝑄 ∈ 𝑇 → ( 𝐾 ∈ dom ( 𝑆 ∖ I ) ↔ 𝐾 ∈ dom ( 𝑄 ∖ I ) ) )
37	36	adantr	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ∈ dom ( 𝑆 ∖ I ) ↔ 𝐾 ∈ dom ( 𝑄 ∖ I ) ) )
38	34 37	mtbird	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ¬ 𝐾 ∈ dom ( 𝑆 ∖ I ) )
39	38	iffalsed	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁 ) → if ( 𝐾 ∈ dom ( 𝑆 ∖ I ) , ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝐾 } ) , 𝐾 ) = 𝐾 )
40	8 39	eqtrd	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑆 ‘ 𝐾 ) = 𝐾 )