Theorem funcnvtp

Description: The converse triple of ordered pairs is a function if the second members are pairwise different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021)

	Ref	Expression
Assertion	funcnvtp	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝐴 ∈ 𝑈 )
2		simp2	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝐶 ∈ 𝑉 )
3		simp1	⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) → 𝐵 ≠ 𝐷 )
4		funcnvpr	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )
5	1 2 3 4	syl2an3an	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )
6		funcnvsn	⊢ Fun ◡ { ⟨ 𝐸 , 𝐹 ⟩ }
7	6	a1i	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) ) → Fun ◡ { ⟨ 𝐸 , 𝐹 ⟩ } )
8		df-rn	⊢ ran { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ }
9		rnpropg	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → ran { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐵 , 𝐷 } )
10	8 9	eqtr3id	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐵 , 𝐷 } )
11	10	3adant3	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐵 , 𝐷 } )
12		df-rn	⊢ ran { ⟨ 𝐸 , 𝐹 ⟩ } = dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ }
13		rnsnopg	⊢ ( 𝐸 ∈ 𝑊 → ran { ⟨ 𝐸 , 𝐹 ⟩ } = { 𝐹 } )
14	12 13	eqtr3id	⊢ ( 𝐸 ∈ 𝑊 → dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ } = { 𝐹 } )
15	14	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ } = { 𝐹 } )
16	11 15	ineq12d	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∩ dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ } ) = ( { 𝐵 , 𝐷 } ∩ { 𝐹 } ) )
17		disjprsn	⊢ ( ( 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) → ( { 𝐵 , 𝐷 } ∩ { 𝐹 } ) = ∅ )
18	17	3adant1	⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) → ( { 𝐵 , 𝐷 } ∩ { 𝐹 } ) = ∅ )
19	16 18	sylan9eq	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) ) → ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∩ dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ } ) = ∅ )
20		funun	⊢ ( ( ( Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∧ Fun ◡ { ⟨ 𝐸 , 𝐹 ⟩ } ) ∧ ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∩ dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ } ) = ∅ ) → Fun ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ ◡ { ⟨ 𝐸 , 𝐹 ⟩ } ) )
21	5 7 19 20	syl21anc	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) ) → Fun ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ ◡ { ⟨ 𝐸 , 𝐹 ⟩ } ) )
22		df-tp	⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ } )
23	22	cnveqi	⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } = ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ } )
24		cnvun	⊢ ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ } ) = ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ ◡ { ⟨ 𝐸 , 𝐹 ⟩ } )
25	23 24	eqtri	⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } = ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ ◡ { ⟨ 𝐸 , 𝐹 ⟩ } )
26	25	funeqi	⊢ ( Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } ↔ Fun ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ ◡ { ⟨ 𝐸 , 𝐹 ⟩ } ) )
27	21 26	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } )