Theorem ex-res

Description: Example for df-res . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

	Ref	Expression
Assertion	ex-res	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( 𝐹 ↾ 𝐵 ) = { ⟨ 2 , 6 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } )
2		df-pr	⊢ { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } = ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } )
3	1 2	eqtrdi	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → 𝐹 = ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } ) )
4	3	reseq1d	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( 𝐹 ↾ 𝐵 ) = ( ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } ) ↾ 𝐵 ) )
5		resundir	⊢ ( ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } ) ↾ 𝐵 ) = ( ( { ⟨ 2 , 6 ⟩ } ↾ 𝐵 ) ∪ ( { ⟨ 3 , 9 ⟩ } ↾ 𝐵 ) )
6	4 5	eqtrdi	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( 𝐹 ↾ 𝐵 ) = ( ( { ⟨ 2 , 6 ⟩ } ↾ 𝐵 ) ∪ ( { ⟨ 3 , 9 ⟩ } ↾ 𝐵 ) ) )
7		2re	⊢ 2 ∈ ℝ
8	7	elexi	⊢ 2 ∈ V
9		6re	⊢ 6 ∈ ℝ
10	9	elexi	⊢ 6 ∈ V
11	8 10	relsnop	⊢ Rel { ⟨ 2 , 6 ⟩ }
12		dmsnopss	⊢ dom { ⟨ 2 , 6 ⟩ } ⊆ { 2 }
13		snsspr2	⊢ { 2 } ⊆ { 1 , 2 }
14		simpr	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → 𝐵 = { 1 , 2 } )
15	13 14	sseqtrrid	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → { 2 } ⊆ 𝐵 )
16	12 15	sstrid	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → dom { ⟨ 2 , 6 ⟩ } ⊆ 𝐵 )
17		relssres	⊢ ( ( Rel { ⟨ 2 , 6 ⟩ } ∧ dom { ⟨ 2 , 6 ⟩ } ⊆ 𝐵 ) → ( { ⟨ 2 , 6 ⟩ } ↾ 𝐵 ) = { ⟨ 2 , 6 ⟩ } )
18	11 16 17	sylancr	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( { ⟨ 2 , 6 ⟩ } ↾ 𝐵 ) = { ⟨ 2 , 6 ⟩ } )
19		1re	⊢ 1 ∈ ℝ
20		1lt3	⊢ 1 < 3
21	19 20	gtneii	⊢ 3 ≠ 1
22		2lt3	⊢ 2 < 3
23	7 22	gtneii	⊢ 3 ≠ 2
24	21 23	nelpri	⊢ ¬ 3 ∈ { 1 , 2 }
25	14	eleq2d	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( 3 ∈ 𝐵 ↔ 3 ∈ { 1 , 2 } ) )
26	24 25	mtbiri	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ¬ 3 ∈ 𝐵 )
27		ressnop0	⊢ ( ¬ 3 ∈ 𝐵 → ( { ⟨ 3 , 9 ⟩ } ↾ 𝐵 ) = ∅ )
28	26 27	syl	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( { ⟨ 3 , 9 ⟩ } ↾ 𝐵 ) = ∅ )
29	18 28	uneq12d	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( ( { ⟨ 2 , 6 ⟩ } ↾ 𝐵 ) ∪ ( { ⟨ 3 , 9 ⟩ } ↾ 𝐵 ) ) = ( { ⟨ 2 , 6 ⟩ } ∪ ∅ ) )
30		un0	⊢ ( { ⟨ 2 , 6 ⟩ } ∪ ∅ ) = { ⟨ 2 , 6 ⟩ }
31	29 30	eqtrdi	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( ( { ⟨ 2 , 6 ⟩ } ↾ 𝐵 ) ∪ ( { ⟨ 3 , 9 ⟩ } ↾ 𝐵 ) ) = { ⟨ 2 , 6 ⟩ } )
32	6 31	eqtrd	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( 𝐹 ↾ 𝐵 ) = { ⟨ 2 , 6 ⟩ } )