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	biimpi	⊢ ( Rel 𝐴 → 𝐴 ⊆ ( V × V ) )
23	22	adantr	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → 𝐴 ⊆ ( V × V ) )
24	23	sselda	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ( V × V ) )
25	24	adantrr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑧 ∈ ( V × V ) )
26	17	ad2antrl	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = ( 1^st ‘ 𝑧 ) )
27		simprr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 )
28	26 27	eqtr3d	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( 1^st ‘ 𝑧 ) = 𝑋 )
29	28 5	sylibr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } )
30	28 29	eqeltrrd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑋 ∈ { 𝑋 } )
31		simpr	⊢ ( ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
32	31	opeq1d	⊢ ( ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) ∧ 𝑥 = 𝑋 ) → ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ )
33	32	eleq1d	⊢ ( ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) ∧ 𝑥 = 𝑋 ) → ( ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ↔ ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ) )
34		1st2nd	⊢ ( ( Rel 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
35	34	ad2ant2r	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
36	28	opeq1d	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ )
37	35 36	eqtrd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑧 = ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ )
38		simprl	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → 𝑧 ∈ 𝐴 )
39	37 38	eqeltrrd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ⟨ 𝑋 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 )
40	30 33 39	rspcedvd	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ∃ 𝑥 ∈ { 𝑋 } ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 )
41		df-rex	⊢ ( ∃ 𝑥 ∈ { 𝑋 } ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑋 } ∧ ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ) )
42	40 41	sylib	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ∃ 𝑥 ( 𝑥 ∈ { 𝑋 } ∧ ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ) )
43		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
44	43	elima3	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑋 } ∧ ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐴 ) )
45	42 44	sylibr	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) )
46	29 45	jca	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) )
47	25 46	jca	⊢ ( ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) → ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) )
48	20 47	impbida	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) )
49		elxp7	⊢ ( 𝑧 ∈ ( { 𝑋 } × ( 𝐴 “ { 𝑋 } ) ) ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) )
50	49	a1i	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑧 ∈ ( { 𝑋 } × ( 𝐴 “ { 𝑋 } ) ) ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ { 𝑋 } ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝐴 “ { 𝑋 } ) ) ) ) )
51		fo1st	⊢ 1^st : V –onto→ V
52		fofn	⊢ ( 1^st : V –onto→ V → 1^st Fn V )
53	51 52	ax-mp	⊢ 1^st Fn V
54		ssv	⊢ 𝐴 ⊆ V
55		fnssres	⊢ ( ( 1^st Fn V ∧ 𝐴 ⊆ V ) → ( 1^st ↾ 𝐴 ) Fn 𝐴 )
56	53 54 55	mp2an	⊢ ( 1^st ↾ 𝐴 ) Fn 𝐴
57		fniniseg	⊢ ( ( 1^st ↾ 𝐴 ) Fn 𝐴 → ( 𝑧 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) )
58	56 57	ax-mp	⊢ ( 𝑧 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) )
59	58	a1i	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑧 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 1^st ↾ 𝐴 ) ‘ 𝑧 ) = 𝑋 ) ) )
60	48 50 59	3bitr4rd	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑧 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) ↔ 𝑧 ∈ ( { 𝑋 } × ( 𝐴 “ { 𝑋 } ) ) ) )
61	60	eqrdv	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑋 } ) = ( { 𝑋 } × ( 𝐴 “ { 𝑋 } ) ) )

Metamath Proof Explorer

Theorem 1stpreimas

Proof