Theorem iunopeqop 5496

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 4809	. 2 ⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}))
2		nfiu1 5003	. . . . . 6 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
3	2	nfeq1 2914	. . . . 5 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩
4		nfv 1914	. . . . 5 ⊢ Ⅎ𝑥∃𝑧 𝐴 = {𝑧}
5	3, 4	nfim 1896	. . . 4 ⊢ Ⅎ𝑥(∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})
6		ssiun2 5023	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → {⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
7		nfcv 2898	. . . . . . . 8 ⊢ Ⅎ𝑥𝑦
8		nfcsb1v 3898	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
9	7, 8	nfop 4865	. . . . . . . . . 10 ⊢ Ⅎ𝑥⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩
10	9	nfsn 4683	. . . . . . . . 9 ⊢ Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}
11	10, 2	nfss 3951	. . . . . . . 8 ⊢ Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
12		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
13		csbeq1a 3888	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
14	12, 13	opeq12d 4857	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝐵⟩ = ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩)
15	14	sneqd 4613	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → {⟨𝑥, 𝐵⟩} = {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩})
16	15	sseq1d 3990	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}))
17	7, 11, 16, 6	vtoclgaf 3555	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 → {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
18	6, 17	anim12i 613	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}))
19		unss 4165	. . . . . . 7 ⊢ (({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
20		sseq2 3985	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩))
21		df-pr 4604	. . . . . . . . . . . 12 ⊢ {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} = ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩})
22	21	eqcomi 2744	. . . . . . . . . . 11 ⊢ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) = {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}
23	22	sseq1i 3987	. . . . . . . . . 10 ⊢ (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ ↔ {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩)
24		vex 3463	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
25		iunopeqop.b	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
26		vex 3463	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
27	25	csbex 5281	. . . . . . . . . . . 12 ⊢ ⦋𝑦 / 𝑥⦌𝐵 ∈ V
28		iunopeqop.c	. . . . . . . . . . . 12 ⊢ 𝐶 ∈ V
29		iunopeqop.d	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ V
30	24, 25, 26, 27, 28, 29	propssopi 5483	. . . . . . . . . . 11 ⊢ ({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → 𝑥 = 𝑦)
31		eqneqall 2943	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ ({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
33	23, 32	sylbi 217	. . . . . . . . 9 ⊢ (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
34	20, 33	biimtrdi 253	. . . . . . . 8 ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))))
35	34	com14 96	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))))
36	19, 35	biimtrid 242	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))))
37	18, 36	mpd 15	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))
38	37	rexlimdva 3141	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))
39	5, 38	rexlimi 3242	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
40		ax-1 6	. . 3 ⊢ (∃𝑧 𝐴 = {𝑧} → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
41	39, 40	jaoi 857	. 2 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}) → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
42	1, 41	syl 17	1 ⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2932  ∃wrex 3060  Vcvv 3459  ⦋csb 3874   ∪ cun 3924   ⊆ wss 3926  ∅c0 4308  {csn 4601  {cpr 4603  ⟨cop 4607  ∪ ciun 4967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-iun 4969

This theorem is referenced by:  funopsn  7138