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

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 ⊢ ( 𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅 )