This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } )