This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝐾 ∈ 𝑁 → ( ¬ 𝐾 ∈ { 𝐾 } → ¬ 𝐾 ∈ 𝑁 ) )
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 imbitrrid ⊢ ( 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 ⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑆 ‘ 𝐾 ) = 𝐾 )