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

Metamath Proof Explorer

Theorem funcnvqp

Description: The converse quadruple 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) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion funcnvqp ( ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ ( 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻 ) ∧ 𝐹 ≠ 𝐻 ) ) → Fun ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 funcnvpr ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )
2 1 3expa ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐵 ≠ 𝐷 ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )
3 2 3ad2antr1 ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )
4 3 ad2ant2r ⊢ ( ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ 𝐹 ≠ 𝐻 ) ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )
5 4 3adantr2 ⊢ ( ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ ( 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻 ) ∧ 𝐹 ≠ 𝐻 ) ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )
6 funcnvpr ⊢ ( ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ∧ 𝐹 ≠ 𝐻 ) → Fun ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } )
7 6 3expa ⊢ ( ( ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 ≠ 𝐻 ) → Fun ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } )
8 7 ad2ant2l ⊢ ( ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ 𝐹 ≠ 𝐻 ) ) → Fun ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } )
9 8 3adantr2 ⊢ ( ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ ( 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻 ) ∧ 𝐹 ≠ 𝐻 ) ) → Fun ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } )
10 df-rn ⊢ ran { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ }
11 rnpropg ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → ran { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐵 , 𝐷 } )
12 10 11 eqtr3id ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐵 , 𝐷 } )
13 df-rn ⊢ ran { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } = dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ }
14 rnpropg ⊢ ( ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) → ran { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } = { 𝐹 , 𝐻 } )
15 13 14 eqtr3id ⊢ ( ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) → dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } = { 𝐹 , 𝐻 } )
16 12 15 ineqan12d ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ) → ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∩ dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) = ( { 𝐵 , 𝐷 } ∩ { 𝐹 , 𝐻 } ) )
17 disjpr2 ⊢ ( ( ( 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹 ) ∧ ( 𝐵 ≠ 𝐻 ∧ 𝐷 ≠ 𝐻 ) ) → ( { 𝐵 , 𝐷 } ∩ { 𝐹 , 𝐻 } ) = ∅ )
18 17 an4s ⊢ ( ( ( 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ ( 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻 ) ) → ( { 𝐵 , 𝐷 } ∩ { 𝐹 , 𝐻 } ) = ∅ )
19 18 3adantl1 ⊢ ( ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ ( 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻 ) ) → ( { 𝐵 , 𝐷 } ∩ { 𝐹 , 𝐻 } ) = ∅ )
20 19 3adant3 ⊢ ( ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ ( 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻 ) ∧ 𝐹 ≠ 𝐻 ) → ( { 𝐵 , 𝐷 } ∩ { 𝐹 , 𝐻 } ) = ∅ )
21 16 20 sylan9eq ⊢ ( ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ ( 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻 ) ∧ 𝐹 ≠ 𝐻 ) ) → ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∩ dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) = ∅ )
22 funun ⊢ ( ( ( Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∧ Fun ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) ∧ ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∩ dom ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) = ∅ ) → Fun ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) )
23 5 9 21 22 syl21anc ⊢ ( ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ ( 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻 ) ∧ 𝐹 ≠ 𝐻 ) ) → Fun ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) )
24 cnvun ⊢ ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) = ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } )
25 24 funeqi ⊢ ( Fun ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) ↔ Fun ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ ◡ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) )
26 23 25 sylibr ⊢ ( ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( ( 𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻 ) ∧ ( 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻 ) ∧ 𝐹 ≠ 𝐻 ) ) → Fun ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ } ) )