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

Metamath Proof Explorer

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 ⟩ } )