fcnvgreu

Description: If the converse of a relation A is a function, exactly one point of its graph has a given second element (that is, function value). (Contributed by Thierry Arnoux, 1-Apr-2018)

		Ref	Expression
	Assertion	fcnvgreu	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑌 ∈ ran 𝐴 ) → ∃! 𝑝 ∈ 𝐴 𝑌 = ( 2^nd ‘ 𝑝 ) )

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝐴 = dom ^◡ 𝐴
2	1	eleq2i	⊢ ( 𝑌 ∈ ran 𝐴 ↔ 𝑌 ∈ dom ^◡ 𝐴 )
3		fgreu	⊢ ( ( Fun ^◡ 𝐴 ∧ 𝑌 ∈ dom ^◡ 𝐴 ) → ∃! 𝑞 ∈ ^◡ 𝐴 𝑌 = ( 1^st ‘ 𝑞 ) )
4	3	adantll	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑌 ∈ dom ^◡ 𝐴 ) → ∃! 𝑞 ∈ ^◡ 𝐴 𝑌 = ( 1^st ‘ 𝑞 ) )
5	2 4	sylan2b	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑌 ∈ ran 𝐴 ) → ∃! 𝑞 ∈ ^◡ 𝐴 𝑌 = ( 1^st ‘ 𝑞 ) )
6		cnvcnvss	⊢ ^◡ ^◡ 𝐴 ⊆ 𝐴
7		cnvssrndm	⊢ ^◡ 𝐴 ⊆ ( ran 𝐴 × dom 𝐴 )
8	7	sseli	⊢ ( 𝑞 ∈ ^◡ 𝐴 → 𝑞 ∈ ( ran 𝐴 × dom 𝐴 ) )
9		dfdm4	⊢ dom 𝐴 = ran ^◡ 𝐴
10	1 9	xpeq12i	⊢ ( ran 𝐴 × dom 𝐴 ) = ( dom ^◡ 𝐴 × ran ^◡ 𝐴 )
11	8 10	eleqtrdi	⊢ ( 𝑞 ∈ ^◡ 𝐴 → 𝑞 ∈ ( dom ^◡ 𝐴 × ran ^◡ 𝐴 ) )
12		2nd1st	⊢ ( 𝑞 ∈ ( dom ^◡ 𝐴 × ran ^◡ 𝐴 ) → ∪ ^◡ { 𝑞 } = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ )
13	11 12	syl	⊢ ( 𝑞 ∈ ^◡ 𝐴 → ∪ ^◡ { 𝑞 } = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ )
14	13	eqcomd	⊢ ( 𝑞 ∈ ^◡ 𝐴 → ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ = ∪ ^◡ { 𝑞 } )
15		relcnv	⊢ Rel ^◡ 𝐴
16		cnvf1olem	⊢ ( ( Rel ^◡ 𝐴 ∧ ( 𝑞 ∈ ^◡ 𝐴 ∧ ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ = ∪ ^◡ { 𝑞 } ) ) → ( ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ∈ ^◡ ^◡ 𝐴 ∧ 𝑞 = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ } ) )
17	16	simpld	⊢ ( ( Rel ^◡ 𝐴 ∧ ( 𝑞 ∈ ^◡ 𝐴 ∧ ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ = ∪ ^◡ { 𝑞 } ) ) → ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ∈ ^◡ ^◡ 𝐴 )
18	15 17	mpan	⊢ ( ( 𝑞 ∈ ^◡ 𝐴 ∧ ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ = ∪ ^◡ { 𝑞 } ) → ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ∈ ^◡ ^◡ 𝐴 )
19	14 18	mpdan	⊢ ( 𝑞 ∈ ^◡ 𝐴 → ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ∈ ^◡ ^◡ 𝐴 )
20	6 19	sseldi	⊢ ( 𝑞 ∈ ^◡ 𝐴 → ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ∈ 𝐴 )
21	20	adantl	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) → ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ∈ 𝐴 )
22		simpll	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → Rel 𝐴 )
23		simpr	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐴 )
24		relssdmrn	⊢ ( Rel 𝐴 → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )
25	24	adantr	⊢ ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )
26	25	sselda	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ( dom 𝐴 × ran 𝐴 ) )
27		2nd1st	⊢ ( 𝑝 ∈ ( dom 𝐴 × ran 𝐴 ) → ∪ ^◡ { 𝑝 } = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ )
28	26 27	syl	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ∪ ^◡ { 𝑝 } = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ )
29	28	eqcomd	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ = ∪ ^◡ { 𝑝 } )
30		cnvf1olem	⊢ ( ( Rel 𝐴 ∧ ( 𝑝 ∈ 𝐴 ∧ ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ = ∪ ^◡ { 𝑝 } ) ) → ( ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ∈ ^◡ 𝐴 ∧ 𝑝 = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ } ) )
31	30	simpld	⊢ ( ( Rel 𝐴 ∧ ( 𝑝 ∈ 𝐴 ∧ ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ = ∪ ^◡ { 𝑝 } ) ) → ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ∈ ^◡ 𝐴 )
32	22 23 29 31	syl12anc	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ∈ ^◡ 𝐴 )
33	15	a1i	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → Rel ^◡ 𝐴 )
34		simplr	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → 𝑞 ∈ ^◡ 𝐴 )
35	14	ad2antlr	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ = ∪ ^◡ { 𝑞 } )
36	16	simprd	⊢ ( ( Rel ^◡ 𝐴 ∧ ( 𝑞 ∈ ^◡ 𝐴 ∧ ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ = ∪ ^◡ { 𝑞 } ) ) → 𝑞 = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ } )
37	33 34 35 36	syl12anc	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → 𝑞 = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ } )
38		simpr	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ )
39	38	sneqd	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → { 𝑝 } = { ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ } )
40	39	cnveqd	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → ^◡ { 𝑝 } = ^◡ { ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ } )
41	40	unieqd	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → ∪ ^◡ { 𝑝 } = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ } )
42	28	ad2antrr	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → ∪ ^◡ { 𝑝 } = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ )
43	37 41 42	3eqtr2d	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ )
44	30	simprd	⊢ ( ( Rel 𝐴 ∧ ( 𝑝 ∈ 𝐴 ∧ ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ = ∪ ^◡ { 𝑝 } ) ) → 𝑝 = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ } )
45	22 23 29 44	syl12anc	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ } )
46	45	ad2antrr	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) → 𝑝 = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ } )
47		simpr	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) → 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ )
48	47	sneqd	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) → { 𝑞 } = { ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ } )
49	48	cnveqd	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) → ^◡ { 𝑞 } = ^◡ { ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ } )
50	49	unieqd	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) → ∪ ^◡ { 𝑞 } = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ } )
51	13	ad2antlr	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) → ∪ ^◡ { 𝑞 } = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ )
52	46 50 51	3eqtr2d	⊢ ( ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) ∧ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) → 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ )
53	43 52	impbida	⊢ ( ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ ^◡ 𝐴 ) → ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) )
54	53	ralrimiva	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ∀ 𝑞 ∈ ^◡ 𝐴 ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) )
55		eqeq2	⊢ ( 𝑟 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ → ( 𝑞 = 𝑟 ↔ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) )
56	55	bibi2d	⊢ ( 𝑟 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ → ( ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = 𝑟 ) ↔ ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) ) )
57	56	ralbidv	⊢ ( 𝑟 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ → ( ∀ 𝑞 ∈ ^◡ 𝐴 ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = 𝑟 ) ↔ ∀ 𝑞 ∈ ^◡ 𝐴 ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) ) )
58	57	rspcev	⊢ ( ( ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ∈ ^◡ 𝐴 ∧ ∀ 𝑞 ∈ ^◡ 𝐴 ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = ⟨ ( 2^nd ‘ 𝑝 ) , ( 1^st ‘ 𝑝 ) ⟩ ) ) → ∃ 𝑟 ∈ ^◡ 𝐴 ∀ 𝑞 ∈ ^◡ 𝐴 ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = 𝑟 ) )
59	32 54 58	syl2anc	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ∃ 𝑟 ∈ ^◡ 𝐴 ∀ 𝑞 ∈ ^◡ 𝐴 ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = 𝑟 ) )
60		reu6	⊢ ( ∃! 𝑞 ∈ ^◡ 𝐴 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ ∃ 𝑟 ∈ ^◡ 𝐴 ∀ 𝑞 ∈ ^◡ 𝐴 ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ↔ 𝑞 = 𝑟 ) )
61	59 60	sylibr	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ∃! 𝑞 ∈ ^◡ 𝐴 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ )
62		fvex	⊢ ( 2^nd ‘ 𝑞 ) ∈ V
63		fvex	⊢ ( 1^st ‘ 𝑞 ) ∈ V
64	62 63	op2ndd	⊢ ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ → ( 2^nd ‘ 𝑝 ) = ( 1^st ‘ 𝑞 ) )
65	64	eqeq2d	⊢ ( 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ → ( 𝑌 = ( 2^nd ‘ 𝑝 ) ↔ 𝑌 = ( 1^st ‘ 𝑞 ) ) )
66	65	adantl	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑝 = ⟨ ( 2^nd ‘ 𝑞 ) , ( 1^st ‘ 𝑞 ) ⟩ ) → ( 𝑌 = ( 2^nd ‘ 𝑝 ) ↔ 𝑌 = ( 1^st ‘ 𝑞 ) ) )
67	21 61 66	reuxfr1d	⊢ ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) → ( ∃! 𝑝 ∈ 𝐴 𝑌 = ( 2^nd ‘ 𝑝 ) ↔ ∃! 𝑞 ∈ ^◡ 𝐴 𝑌 = ( 1^st ‘ 𝑞 ) ) )
68	67	adantr	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑌 ∈ ran 𝐴 ) → ( ∃! 𝑝 ∈ 𝐴 𝑌 = ( 2^nd ‘ 𝑝 ) ↔ ∃! 𝑞 ∈ ^◡ 𝐴 𝑌 = ( 1^st ‘ 𝑞 ) ) )
69	5 68	mpbird	⊢ ( ( ( Rel 𝐴 ∧ Fun ^◡ 𝐴 ) ∧ 𝑌 ∈ ran 𝐴 ) → ∃! 𝑝 ∈ 𝐴 𝑌 = ( 2^nd ‘ 𝑝 ) )

Metamath Proof Explorer

Theorem fcnvgreu

Proof