Theorem iunopeqopOLD 5503

Description: Obsolete version of iunopeqop 5502 as of 9-May-2026. (Contributed by AV, 20-Sep-2020.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypotheses

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

Assertion

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

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

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

Proof of Theorem iunopeqopOLD

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0snor2el 4796	. 2 ⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}))
2		nfiu1 4990	. . . . . 6 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
3	2	nfeq1 2939	. . . . 5 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩
4		nfv 1947	. . . . 5 ⊢ Ⅎ𝑥∃𝑧 𝐴 = {𝑧}
5	3, 4	nfim 1929	. . . 4 ⊢ Ⅎ𝑥(∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})
6		ssiun2 5010	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → {⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
7		nfcv 2924	. . . . . . . 8 ⊢ Ⅎ𝑥𝑦
8		nfcsb1v 3874	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
9	7, 8	nfop 4852	. . . . . . . . . 10 ⊢ Ⅎ𝑥⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩
10	9	nfsn 4671	. . . . . . . . 9 ⊢ Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}
11	10, 2	nfss 3927	. . . . . . . 8 ⊢ Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
12		id 23	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
13		csbeq1a 3864	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
14	12, 13	opeq12d 4844	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝐵⟩ = ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩)
15	14	sneqd 4599	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → {⟨𝑥, 𝐵⟩} = {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩})
16	15	sseq1d 3965	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}))
17	7, 11, 16, 6	vtoclgaf 3538	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 → {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
18	6, 17	anim12i 625	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}))
19		unss 4139	. . . . . . 7 ⊢ (({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})
20		sseq2 3960	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩))
21		df-pr 4590	. . . . . . . . . . . 12 ⊢ {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} = ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩})
22	21	eqcomi 2771	. . . . . . . . . . 11 ⊢ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) = {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}
23	22	sseq1i 3962	. . . . . . . . . 10 ⊢ (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ ↔ {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩)
24		vex 3457	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
25		iunopeqop.b	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
26		vex 3457	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
27	25	csbex 5272	. . . . . . . . . . . 12 ⊢ ⦋𝑦 / 𝑥⦌𝐵 ∈ V
28		iunopeqop.c	. . . . . . . . . . . 12 ⊢ 𝐶 ∈ V
29		iunopeqop.d	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ V
30	24, 25, 26, 27, 28, 29	propssopi 5489	. . . . . . . . . . 11 ⊢ ({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → 𝑥 = 𝑦)
31		eqneqall 2968	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
32	30, 31	syl 18	. . . . . . . . . 10 ⊢ ({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
33	23, 32	sylbi 220	. . . . . . . . 9 ⊢ (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))
34	20, 33	biimtrdi 256	. . . . . . . 8 ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))))
35	34	com14 97	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))))
36	19, 35	biimtrid 245	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))))
37	18, 36	mpd 16	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))
38	37	rexlimdva 3165	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))
39	5, 38	rexlimi 3264	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
40		ax-1 6	. . 3 ⊢ (∃𝑧 𝐴 = {𝑧} → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
41	39, 40	jaoi 871	. 2 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}) → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
42	1, 41	syl 18	1 ⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))

This proof depends on syntax axioms:   → 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:  funopsnOLD  7149