Theorem iunopeqop

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

	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		n0snor2el	⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃ 𝑧 𝐴 = { 𝑧 } ) )
5		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }
6	5	nfeq1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩
7		nfv	⊢ Ⅎ 𝑥 ∃ 𝑧 𝐴 = { 𝑧 }
8	6 7	nfim	⊢ Ⅎ 𝑥 ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } )
9		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } )
10		nfcv	⊢ Ⅎ 𝑥 𝑦
11		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
12	10 11	nfop	⊢ Ⅎ 𝑥 ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩
13	12	nfsn	⊢ Ⅎ 𝑥 { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ }
14	13 5	nfss	⊢ Ⅎ 𝑥 { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }
15		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
16		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
17	15 16	opeq12d	⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝐵 ⟩ = ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
18	17	sneqd	⊢ ( 𝑥 = 𝑦 → { ⟨ 𝑥 , 𝐵 ⟩ } = { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } )
19	18	sseq1d	⊢ ( 𝑥 = 𝑦 → ( { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ↔ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ) )
20	10 14 19 9	vtoclgaf	⊢ ( 𝑦 ∈ 𝐴 → { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } )
21	9 20	anim12i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ∧ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ) )
22		unss	⊢ ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ∧ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ) ↔ ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } )
23		sseq2	⊢ ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ↔ ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ⟨ 𝐶 , 𝐷 ⟩ ) )
24		df-pr	⊢ { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } = ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } )
25	24	eqcomi	⊢ ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) = { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ }
26	25	sseq1i	⊢ ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ⟨ 𝐶 , 𝐷 ⟩ ↔ { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ⟨ 𝐶 , 𝐷 ⟩ )
27		vex	⊢ 𝑥 ∈ V
28		vex	⊢ 𝑦 ∈ V
29	1	csbex	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ V
30	27 1 28 29 2 3	propssopi	⊢ ( { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ⟨ 𝐶 , 𝐷 ⟩ → 𝑥 = 𝑦 )
31		eqneqall	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
32	30 31	syl	⊢ ( { ⟨ 𝑥 , 𝐵 ⟩ , ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
33	26 32	sylbi	⊢ ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
34	23 33	biimtrdi	⊢ ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } → ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 𝐴 = { 𝑧 } ) ) ) )
35	34	com14	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ∪ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ) ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } → ( 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) ) ) )
36	22 35	biimtrid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( { ⟨ 𝑥 , 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ∧ { ⟨ 𝑦 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ } ⊆ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } ) → ( 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) ) ) )
37	21 36	mpd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
38	37	rexlimdva	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) ) )
39	8 38	rexlimi	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) )
40		ax-1	⊢ ( ∃ 𝑧 𝐴 = { 𝑧 } → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) )
41	39 40	jaoi	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃ 𝑧 𝐴 = { 𝑧 } ) → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) )
42	4 41	syl	⊢ ( 𝐴 ≠ ∅ → ( ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ∃ 𝑧 𝐴 = { 𝑧 } ) )