Theorem iunopeqop 5404

Description: Implication of an ordered pair being equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020.) (Avoid depending on this detail.)

Hypotheses

Ref	Expression
iunopeqop.b	⊢ 𝐵 ∈ V
iunopeqop.c	⊢ 𝐶 ∈ V
iunopeqop.d	⊢ 𝐷 ∈ V

Assertion

Ref	Expression
iunopeqop	⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))

Distinct variable groups:   𝑥,𝐴,𝑧   𝑥,𝐶   𝑥,𝐷

Allowed substitution hints:   𝐵(𝑥,𝑧)   𝐶(𝑧)   𝐷(𝑧)

Proof of Theorem iunopeqop

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0snor2el 4744	. 2 ⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}))
2		nfiu1 4938	. . . . . 6 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
3	2	nfeq1 2919	. . . . 5 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩
4		nfv 1922	. . . . 5 ⊢ Ⅎ𝑥∃𝑧 𝐴 = {𝑧}
5	3, 4	nfim 1904	. . . 4 ⊢ Ⅎ𝑥(∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})
6		ssiun2 4956	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → {⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
7		nfcv 2904	. . . . . . . 8 ⊢ Ⅎ𝑥𝑦
8		nfcsb1v 3836	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
9	7, 8	nfop 4800	. . . . . . . . . 10 ⊢ Ⅎ𝑥⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩
10	9	nfsn 4623	. . . . . . . . 9 ⊢ Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}
11	10, 2	nfss 3892	. . . . . . . 8 ⊢ Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
12		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
13		csbeq1a 3825	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
14	12, 13	opeq12d 4792	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝐵⟩ = ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩)
15	14	sneqd 4553	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → {⟨𝑥, 𝐵⟩} = {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩})
16	15	sseq1d 3932	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}))
17	7, 11, 16, 6	vtoclgaf 3488	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 → {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
18	6, 17	anim12i 616	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}))
19		unss 4098	. . . . . . 7 ⊢ (({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
20		sseq2 3927	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩))
21		df-pr 4544	. . . . . . . . . . . 12 ⊢ {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} = ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩})
22	21	eqcomi 2746	. . . . . . . . . . 11 ⊢ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) = {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}
23	22	sseq1i 3929	. . . . . . . . . 10 ⊢ (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ ↔ {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩)
24		vex 3412	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
25		iunopeqop.b	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
26		vex 3412	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
27	25	csbex 5204	. . . . . . . . . . . 12 ⊢ ⦋𝑦 / 𝑥⦌𝐵 ∈ V
28		iunopeqop.c	. . . . . . . . . . . 12 ⊢ 𝐶 ∈ V
29		iunopeqop.d	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ V
30	24, 25, 26, 27, 28, 29	propssopi 5391	. . . . . . . . . . 11 ⊢ ({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → 𝑥 = 𝑦)
31		eqneqall 2951	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ ({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
33	23, 32	sylbi 220	. . . . . . . . 9 ⊢ (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
34	20, 33	syl6bi 256	. . . . . . . 8 ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))))
35	34	com14 96	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))))
36	19, 35	syl5bi 245	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))))
37	18, 36	mpd 15	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))
38	37	rexlimdva 3203	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))
39	5, 38	rexlimi 3234	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
40		ax-1 6	. . 3 ⊢ (∃𝑧 𝐴 = {𝑧} → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
41	39, 40	jaoi 857	. 2 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}) → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
42	1, 41	syl 17	1 ⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 847   = wceq 1543  ∃wex 1787   ∈ wcel 2110   ≠ wne 2940  ∃wrex 3062  Vcvv 3408  ⦋csb 3811   ∪ cun 3864   ⊆ wss 3866  ∅c0 4237  {csn 4541  {cpr 4543  ⟨cop 4547  ∪ ciun 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-iun 4906

This theorem is referenced by:  funopsn  6963