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	syl5eq	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 )
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 ( 𝑌 = 𝑍 , ∅ , { 𝑋 } ) )