1stpreimas

Description: The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020)

		Ref	Expression
	Assertion	1stpreimas	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) = ( { 𝑋 } × ( 𝐴 “ { 𝑋 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		1st2ndb	⊢ ( 𝑧 ∈ ( V × V ) ↔ 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
2	1	biimpi	⊢ ( 𝑧 ∈ ( V × V ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
3	2	ad2antrl	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
4		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
5	4	elsn	⊢ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ↔ ( 1^st ‘ 𝑧 ) = 𝑋 )
6	5	biimpi	⊢ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } → ( 1^st ‘ 𝑧 ) = 𝑋 )
7	6	ad2antrl	⊢ ( ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) → ( 1^st ‘ 𝑧 ) = 𝑋 )
8	7	adantl	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → ( 1^st ‘ 𝑧 ) = 𝑋 )
9	8	opeq1d	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ )
10	3 9	eqtrd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → 𝑧 = ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ )
11		simplr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → 𝑋 ∈ 𝑉 )
12		simprrr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) )
13		elimasng	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) → ( ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ↔ ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ) )
14	13	biimpa	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) → ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 )
15	11 12 12 14	syl21anc	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 )
16	10 15	eqeltrd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → 𝑧 ∈ 𝐴 )
17		fvres	⊢ ( 𝑧 ∈ 𝐴 → ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = ( 1^st ‘ 𝑧 ) )
18	16 17	syl	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = ( 1^st ‘ 𝑧 ) )
19	18 8	eqtrd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 )
20	16 19	jca	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) → ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) )
21		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
22	21	birani	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → 𝐴 ⊆ ( V × V ) )
23	22	sselda	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ( V × V ) )
24	23	adantrr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑧 ∈ ( V × V ) )
25	17	ad2antrl	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = ( 1^st ‘ 𝑧 ) )
26		simprr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 )
27	25 26	eqtr3d	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( 1^st ‘ 𝑧 ) = 𝑋 )
28	27 5	sylibr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } )
29	27 28	eqeltrrd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑋 ∈ { 𝑋 } )
30		simpr	⊢ ( ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
31	30	opeq1d	⊢ ( ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) ∧ 𝑥 = 𝑋 ) → ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ )
32	31	eleq1d	⊢ ( ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) ∧ 𝑥 = 𝑋 ) → ( ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ↔ ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ) )
33		1st2nd	⊢ ( ( Rel 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
34	33	ad2ant2r	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
35	27	opeq1d	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ )
36	34 35	eqtrd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑧 = ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ )
37		simprl	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑧 ∈ 𝐴 )
38	36 37	eqeltrrd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 )
39	29 32 38	rspcedvd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ∃ 𝑥 ∈ { 𝑋 } ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 )
40		df-rex	⊢ ( ∃ 𝑥 ∈ { 𝑋 } ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑋 } ∧ ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ) )
41	39 40	sylib	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ∃ 𝑥 ( 𝑥 ∈ { 𝑋 } ∧ ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ) )
42		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
43	42	elima3	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑋 } ∧ ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ) )
44	41 43	sylibr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) )
45	28 44	jca	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) )
46	24 45	jca	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) )
47	20 46	impbida	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) )
48		elxp7	⊢ ( 𝑧 ∈ ( { 𝑋 } × ( 𝐴 “ { 𝑋 } ) ) ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) )
49	48	a1i	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑧 ∈ ( { 𝑋 } × ( 𝐴 “ { 𝑋 } ) ) ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) )
50		fo1st	⊢ 1^st : V –onto→ V
51		fofn	⊢ ( 1^st : V –onto→ V → 1^st Fn V )
52	50 51	ax-mp	⊢ 1^st Fn V
53		ssv	⊢ 𝐴 ⊆ V
54		fnssres	⊢ ( ( 1^st Fn V ∧ 𝐴 ⊆ V ) → ( 1^st ↾ 𝐴 ) Fn 𝐴 )
55	52 53 54	mp2an	⊢ ( 1^st ↾ 𝐴 ) Fn 𝐴
56		fniniseg	⊢ ( ( 1^st ↾ 𝐴 ) Fn 𝐴 → ( 𝑧 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) )
57	55 56	ax-mp	⊢ ( 𝑧 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) )
58	57	a1i	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑧 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) )
59	47 49 58	3bitr4rd	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑧 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) ↔ 𝑧 ∈ ( { 𝑋 } × ( 𝐴 “ { 𝑋 } ) ) ) )
60	59	eqrdv	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) = ( { 𝑋 } × ( 𝐴 “ { 𝑋 } ) ) )

Metamath Proof Explorer

Theorem 1stpreimas

Proof