Theorem funcnvtp 6595

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.)

Assertion

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

Proof of Theorem funcnvtp

Step	Hyp	Ref	Expression
1		simp1 1154	. . . 4 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → 𝐴 ∈ 𝑈)
2		simp2 1155	. . . 4 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → 𝐶 ∈ 𝑉)
3		simp1 1154	. . . 4 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹) → 𝐵 ≠ 𝐷)
4		funcnvpr 6594	. . . 4 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩})
5	1, 2, 3, 4	syl2an3an 1449	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩})
6		funcnvsn 6582	. . . 4 ⊢ Fun ◡{⟨𝐸, 𝐹⟩}
7	6	a1i 11	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun ◡{⟨𝐸, 𝐹⟩})
8		df-rn 5662	. . . . . . 7 ⊢ ran {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}
9		rnpropg 6216	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → ran {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐵, 𝐷})
10	8, 9	eqtr3id 2810	. . . . . 6 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐵, 𝐷})
11	10	3adant3 1150	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐵, 𝐷})
12		df-rn 5662	. . . . . . 7 ⊢ ran {⟨𝐸, 𝐹⟩} = dom ◡{⟨𝐸, 𝐹⟩}
13		rnsnopg 6215	. . . . . . 7 ⊢ (𝐸 ∈ 𝑊 → ran {⟨𝐸, 𝐹⟩} = {𝐹})
14	12, 13	eqtr3id 2810	. . . . . 6 ⊢ (𝐸 ∈ 𝑊 → dom ◡{⟨𝐸, 𝐹⟩} = {𝐹})
15	14	3ad2ant3 1153	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom ◡{⟨𝐸, 𝐹⟩} = {𝐹})
16	11, 15	ineq12d 4167	. . . 4 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∩ dom ◡{⟨𝐸, 𝐹⟩}) = ({𝐵, 𝐷} ∩ {𝐹}))
17		disjprsn 4675	. . . . 5 ⊢ ((𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹) → ({𝐵, 𝐷} ∩ {𝐹}) = ∅)
18	17	3adant1 1148	. . . 4 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹) → ({𝐵, 𝐷} ∩ {𝐹}) = ∅)
19	16, 18	sylan9eq 2816	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → (dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∩ dom ◡{⟨𝐸, 𝐹⟩}) = ∅)
20		funun 6578	. . 3 ⊢ (((Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∧ Fun ◡{⟨𝐸, 𝐹⟩}) ∧ (dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∩ dom ◡{⟨𝐸, 𝐹⟩}) = ∅) → Fun (◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ ◡{⟨𝐸, 𝐹⟩}))
21	5, 7, 19, 20	syl21anc 851	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun (◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ ◡{⟨𝐸, 𝐹⟩}))
22		df-tp 4589	. . . . 5 ⊢ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ {⟨𝐸, 𝐹⟩})
23	22	cnveqi 5852	. . . 4 ⊢ ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = ◡({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ {⟨𝐸, 𝐹⟩})
24		cnvun 6131	. . . 4 ⊢ ◡({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ {⟨𝐸, 𝐹⟩}) = (◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ ◡{⟨𝐸, 𝐹⟩})
25	23, 24	eqtri 2784	. . 3 ⊢ ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = (◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ ◡{⟨𝐸, 𝐹⟩})
26	25	funeqi 6552	. 2 ⊢ (Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} ↔ Fun (◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ ◡{⟨𝐸, 𝐹⟩}))
27	21, 26	sylibr 237	1 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956   ∪ cun 3897   ∩ cin 3898  ∅c0 4279  {csn 4584  {cpr 4586  {ctp 4588  ⟨cop 4590  ^◡ccnv 5650  dom cdm 5651  ran crn 5652  Fun wfun 6525

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6533

This theorem is used by:  funcnvs3  15045