iunopeqop

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

	Ref	Expression
Hypotheses	iunopeqop.b	⊢ 𝐵 ∈ V
	iunopeqop.c	⊢ 𝐶 ∈ V
	iunopeqop.d	⊢ 𝐷 ∈ V
Assertion	iunopeqop	⊢ ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } )

Proof

Step	Hyp	Ref	Expression
1		iunopeqop.b	⊢ 𝐵 ∈ V
2		iunopeqop.c	⊢ 𝐶 ∈ V
3		iunopeqop.d	⊢ 𝐷 ∈ V
4	2 3	opnzi	⊢ ⟨ 𝐶 , 𝐷 ⟩ ≠ ∅
5	4	a1i	⊢ ( 𝐴 = ∅ → ⟨ 𝐶 , 𝐷 ⟩ ≠ ∅ )
6		iuneq1	⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ∪ 𝑥 ∈ ∅ { ⟨ 𝑥 , 𝐵 ⟩ } )
7		0iun	⊢ ∪ 𝑥 ∈ ∅ { ⟨ 𝑥 , 𝐵 ⟩ } = ∅
8	6 7	eqtrdi	⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ∅ )
9	5 8	neeqtrrd	⊢ ( 𝐴 = ∅ → ⟨ 𝐶 , 𝐷 ⟩ ≠ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } )
10		nesym	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ≠ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ↔ ¬ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ )
11	9 10	sylib	⊢ ( 𝐴 = ∅ → ¬ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ )
12	11	pm2.21d	⊢ ( 𝐴 = ∅ → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) )
13		n0snor2el	⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃ 𝑧 𝐴 = { 𝑧 } ) )
14		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }
15	14	nfeq1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩
16		nfv	⊢ Ⅎ 𝑥 ∃ 𝑧 𝐴 = { 𝑧 }
17	15 16	nfim	⊢ Ⅎ 𝑥 ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } )
18		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } )
19		nfcv	⊢ Ⅎ 𝑥 𝑦
20		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
21	19 20	nfop	⊢ Ⅎ 𝑥 ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩
22	21	nfsn	⊢ Ⅎ 𝑥 { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ }
23	22 14	nfss	⊢ Ⅎ 𝑥 { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }
24		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
25		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
26	24 25	opeq12d	⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝐵 ⟩ = ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
27	26	sneqd	⊢ ( 𝑥 = 𝑦 → { ⟨ 𝑥 , 𝐵 ⟩ } = { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } )
28	27	sseq1d	⊢ ( 𝑥 = 𝑦 → ( { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ↔ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ) )
29	19 23 28 18	vtoclgaf	⊢ ( 𝑦 ∈ 𝐴 → { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } )
30	18 29	anim12i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ∧ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ) )
31		unss	⊢ ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ∧ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ) ↔ ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } )
32		sseq2	⊢ ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ↔ ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ⟨ 𝐶 , 𝐷 ⟩ ) )
33		df-pr	⊢ { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } = ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } )
34	33	eqcomi	⊢ ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) = { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ }
35	34	sseq1i	⊢ ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ⟨ 𝐶 , 𝐷 ⟩ ↔ { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ⟨ 𝐶 , 𝐷 ⟩ )
36		vex	⊢ 𝑥 ∈ V
37		vex	⊢ 𝑦 ∈ V
38	1	csbex	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ V
39	36 1 37 38 2 3	propssopi	⊢ ( { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ⟨ 𝐶 , 𝐷 ⟩ → 𝑥 = 𝑦 )
40		eqneqall	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
41	39 40	syl	⊢ ( { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
42	35 41	sylbi	⊢ ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
43	32 42	biimtrdi	⊢ ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } → ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 𝐴 = { 𝑧 } ) ) ) )
44	43	com14	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } → ( 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) ) ) )
45	31 44	biimtrid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ∧ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ) → ( 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) ) ) )
46	30 45	mpd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
47	46	rexlimdva	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
48	17 47	rexlimi	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) )
49		ax-1	⊢ ( ∃ 𝑧 𝐴 = { 𝑧 } → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) )
50	48 49	jaoi	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃ 𝑧 𝐴 = { 𝑧 } ) → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) )
51	13 50	syl	⊢ ( 𝐴 ≠ ∅ → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) )
52	12 51	pm2.61ine	⊢ ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } )

Metamath Proof Explorer

Theorem iunopeqop

Proof