Theorem iunopeqop 5502

Description: Implication of an ordered pair being equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020.) Remove antecedent. (Revised by Eric Schmidt, 9-May-2026.) (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		iunopeqop.c	. . . . . . 7 ⊢ 𝐶 ∈ V
2		iunopeqop.d	. . . . . . 7 ⊢ 𝐷 ∈ V
3	1, 2	opnzi 5454	. . . . . 6 ⊢ ⟨𝐶, 𝐷⟩ ≠ ∅
4	3	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → ⟨𝐶, 𝐷⟩ ≠ ∅)
5		iuneq1 4971	. . . . . 6 ⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ∪ 𝑥 ∈ ∅ {⟨𝑥, 𝐵⟩})
6		0iun 5025	. . . . . 6 ⊢ ∪ 𝑥 ∈ ∅ {⟨𝑥, 𝐵⟩} = ∅
7	5, 6	eqtrdi 2813	. . . . 5 ⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ∅)
8	4, 7	neeqtrrd 3031	. . . 4 ⊢ (𝐴 = ∅ → ⟨𝐶, 𝐷⟩ ≠ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
9		nesym 3013	. . . 4 ⊢ (⟨𝐶, 𝐷⟩ ≠ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ ¬ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩)
10	8, 9	sylib 221	. . 3 ⊢ (𝐴 = ∅ → ¬ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩)
11	10	pm2.21d 122	. 2 ⊢ (𝐴 = ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
12		n0snor2el 4796	. . 3 ⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}))
13		nfiu1 4990	. . . . . . 7 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
14	13	nfeq1 2939	. . . . . 6 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩
15		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑥∃𝑧 𝐴 = {𝑧}
16	14, 15	nfim 1929	. . . . 5 ⊢ Ⅎ𝑥(∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})
17		ssiun2 5010	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → {⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
18		nfcv 2924	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑦
19		nfcsb1v 3874	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
20	18, 19	nfop 4852	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩
21	20	nfsn 4671	. . . . . . . . . 10 ⊢ Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}
22	21, 13	nfss 3927	. . . . . . . . 9 ⊢ Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
23		id 23	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
24		csbeq1a 3864	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
25	23, 24	opeq12d 4844	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝐵⟩ = ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩)
26	25	sneqd 4599	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → {⟨𝑥, 𝐵⟩} = {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩})
27	26	sseq1d 3965	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}))
28	18, 22, 27, 17	vtoclgaf 3538	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐴 → {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
29	17, 28	anim12i 625	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}))
30		unss 4139	. . . . . . . 8 ⊢ (({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
31		sseq2 3960	. . . . . . . . . 10 ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩))
32		df-pr 4590	. . . . . . . . . . . . 13 ⊢ {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} = ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩})
33	32	eqcomi 2771	. . . . . . . . . . . 12 ⊢ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) = {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}
34	33	sseq1i 3962	. . . . . . . . . . 11 ⊢ (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ ↔ {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩)
35		vex 3457	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
36		iunopeqop.b	. . . . . . . . . . . . 13 ⊢ 𝐵 ∈ V
37		vex 3457	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
38	36	csbex 5272	. . . . . . . . . . . . 13 ⊢ ⦋𝑦 / 𝑥⦌𝐵 ∈ V
39	35, 36, 37, 38, 1, 2	propssopi 5489	. . . . . . . . . . . 12 ⊢ ({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → 𝑥 = 𝑦)
40		eqneqall 2968	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
41	39, 40	syl 18	. . . . . . . . . . 11 ⊢ ({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
42	34, 41	sylbi 220	. . . . . . . . . 10 ⊢ (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
43	31, 42	biimtrdi 256	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))))
44	43	com14 97	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))))
45	30, 44	biimtrid 245	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))))
46	29, 45	mpd 16	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))
47	46	rexlimdva 3165	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))
48	16, 47	rexlimi 3264	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
49		ax-1 6	. . . 4 ⊢ (∃𝑧 𝐴 = {𝑧} → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
50	48, 49	jaoi 871	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}) → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
51	12, 50	syl 18	. 2 ⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
52	11, 51	pm2.61ine 3040	1 ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2957  ∃wrex 3088  Vcvv 3453  ⦋csb 3850   ∪ cun 3900   ⊆ wss 3902  ∅c0 4282  {csn 4587  {cpr 4589  ⟨cop 4593  ∪ ciun 4954

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-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-iun 4956

This theorem is used by:  funopsn  7147