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