Metamath Proof Explorer


Theorem pmtrdifellem1

Description: Lemma 1 for pmtrdifel . (Contributed by AV, 15-Jan-2019)

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

Proof

Step Hyp Ref Expression
1 pmtrdifel.t 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
2 pmtrdifel.r 𝑅 = ran ( pmTrsp ‘ 𝑁 )
3 pmtrdifel.0 𝑆 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) )
4 eqid ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
5 4 1 pmtrfb ( 𝑄𝑇 ↔ ( ( 𝑁 ∖ { 𝐾 } ) ∈ V ∧ 𝑄 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) )
6 difsnexi ( ( 𝑁 ∖ { 𝐾 } ) ∈ V → 𝑁 ∈ V )
7 f1of ( 𝑄 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) → 𝑄 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) )
8 fdm ( 𝑄 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) → dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) )
9 difssd ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → ( 𝑄 ∖ I ) ⊆ 𝑄 )
10 dmss ( ( 𝑄 ∖ I ) ⊆ 𝑄 → dom ( 𝑄 ∖ I ) ⊆ dom 𝑄 )
11 9 10 syl ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → dom ( 𝑄 ∖ I ) ⊆ dom 𝑄 )
12 difssd ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 )
13 sseq1 ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → ( dom 𝑄𝑁 ↔ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) )
14 12 13 mpbird ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → dom 𝑄𝑁 )
15 11 14 sstrd ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → dom ( 𝑄 ∖ I ) ⊆ 𝑁 )
16 7 8 15 3syl ( 𝑄 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) → dom ( 𝑄 ∖ I ) ⊆ 𝑁 )
17 id ( dom ( 𝑄 ∖ I ) ≈ 2o → dom ( 𝑄 ∖ I ) ≈ 2o )
18 eqid ( pmTrsp ‘ 𝑁 ) = ( pmTrsp ‘ 𝑁 )
19 18 2 pmtrrn ( ( 𝑁 ∈ V ∧ dom ( 𝑄 ∖ I ) ⊆ 𝑁 ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) → ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) ) ∈ 𝑅 )
20 3 19 eqeltrid ( ( 𝑁 ∈ V ∧ dom ( 𝑄 ∖ I ) ⊆ 𝑁 ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) → 𝑆𝑅 )
21 6 16 17 20 syl3an ( ( ( 𝑁 ∖ { 𝐾 } ) ∈ V ∧ 𝑄 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) → 𝑆𝑅 )
22 5 21 sylbi ( 𝑄𝑇𝑆𝑅 )