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