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

Metamath Proof Explorer

Theorem suppsnop

Description: The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019)

Ref Expression
Hypothesis suppsnop.f ⊢ 𝐹 = { ⟨ 𝑋 , 𝑌 ⟩ }
Assertion suppsnop ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( 𝐹 supp 𝑍 ) = if ( 𝑌 = 𝑍 , ∅ , { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 suppsnop.f ⊢ 𝐹 = { ⟨ 𝑋 , 𝑌 ⟩ }
2 f1osng ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } –1-1-onto→ { 𝑌 } )
3 f1of ⊢ ( { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } –1-1-onto→ { 𝑌 } → { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } ⟶ { 𝑌 } )
4 2 3 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } ⟶ { 𝑌 } )
5 4 3adant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } ⟶ { 𝑌 } )
6 1 feq1i ⊢ ( 𝐹 : { 𝑋 } ⟶ { 𝑌 } ↔ { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } ⟶ { 𝑌 } )
7 5 6 sylibr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → 𝐹 : { 𝑋 } ⟶ { 𝑌 } )
8 snex ⊢ { 𝑋 } ∈ V
9 fex ⊢ ( ( 𝐹 : { 𝑋 } ⟶ { 𝑌 } ∧ { 𝑋 } ∈ V ) → 𝐹 ∈ V )
10 7 8 9 sylancl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → 𝐹 ∈ V )
11 simp3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → 𝑍 ∈ 𝑈 )
12 suppval ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑈 ) → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } } )
13 10 11 12 syl2anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } } )
14 7 fdmd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → dom 𝐹 = { 𝑋 } )
15 14 rabeqdv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } } = { 𝑥 ∈ { 𝑋 } ∣ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } } )
16 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
17 16 imaeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐹 “ { 𝑥 } ) = ( 𝐹 “ { 𝑋 } ) )
18 17 neeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ↔ ( 𝐹 “ { 𝑋 } ) ≠ { 𝑍 } ) )
19 18 rabsnif ⊢ { 𝑥 ∈ { 𝑋 } ∣ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } } = if ( ( 𝐹 “ { 𝑋 } ) ≠ { 𝑍 } , { 𝑋 } , ∅ )
20 15 19 eqtrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } } = if ( ( 𝐹 “ { 𝑋 } ) ≠ { 𝑍 } , { 𝑋 } , ∅ ) )
21 7 ffnd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → 𝐹 Fn { 𝑋 } )
22 snidg ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
23 22 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → 𝑋 ∈ { 𝑋 } )
24 fnsnfv ⊢ ( ( 𝐹 Fn { 𝑋 } ∧ 𝑋 ∈ { 𝑋 } ) → { ( 𝐹 ‘ 𝑋 ) } = ( 𝐹 “ { 𝑋 } ) )
25 24 eqcomd ⊢ ( ( 𝐹 Fn { 𝑋 } ∧ 𝑋 ∈ { 𝑋 } ) → ( 𝐹 “ { 𝑋 } ) = { ( 𝐹 ‘ 𝑋 ) } )
26 21 23 25 syl2anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( 𝐹 “ { 𝑋 } ) = { ( 𝐹 ‘ 𝑋 ) } )
27 26 neeq1d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( ( 𝐹 “ { 𝑋 } ) ≠ { 𝑍 } ↔ { ( 𝐹 ‘ 𝑋 ) } ≠ { 𝑍 } ) )
28 1 fveq1i ⊢ ( 𝐹 ‘ 𝑋 ) = ( { ⟨ 𝑋 , 𝑌 ⟩ } ‘ 𝑋 )
29 fvsng ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } ‘ 𝑋 ) = 𝑌 )
30 29 3adant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } ‘ 𝑋 ) = 𝑌 )
31 28 30 eqtrid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 )
32 31 sneqd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → { ( 𝐹 ‘ 𝑋 ) } = { 𝑌 } )
33 32 neeq1d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( { ( 𝐹 ‘ 𝑋 ) } ≠ { 𝑍 } ↔ { 𝑌 } ≠ { 𝑍 } ) )
34 sneqbg ⊢ ( 𝑌 ∈ 𝑊 → ( { 𝑌 } = { 𝑍 } ↔ 𝑌 = 𝑍 ) )
35 34 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( { 𝑌 } = { 𝑍 } ↔ 𝑌 = 𝑍 ) )
36 35 necon3abid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( { 𝑌 } ≠ { 𝑍 } ↔ ¬ 𝑌 = 𝑍 ) )
37 27 33 36 3bitrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( ( 𝐹 “ { 𝑋 } ) ≠ { 𝑍 } ↔ ¬ 𝑌 = 𝑍 ) )
38 37 ifbid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → if ( ( 𝐹 “ { 𝑋 } ) ≠ { 𝑍 } , { 𝑋 } , ∅ ) = if ( ¬ 𝑌 = 𝑍 , { 𝑋 } , ∅ ) )
39 ifnot ⊢ if ( ¬ 𝑌 = 𝑍 , { 𝑋 } , ∅ ) = if ( 𝑌 = 𝑍 , ∅ , { 𝑋 } )
40 38 39 eqtrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → if ( ( 𝐹 “ { 𝑋 } ) ≠ { 𝑍 } , { 𝑋 } , ∅ ) = if ( 𝑌 = 𝑍 , ∅ , { 𝑋 } ) )
41 13 20 40 3eqtrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( 𝐹 supp 𝑍 ) = if ( 𝑌 = 𝑍 , ∅ , { 𝑋 } ) )