Theorem funsndifnop

Description: A singleton of an ordered pair is not an ordered pair if the components are different. (Contributed by AV, 23-Sep-2020) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	funsndifnop.a	⊢ 𝐴 ∈ V
	funsndifnop.b	⊢ 𝐵 ∈ V
	funsndifnop.g	⊢ 𝐺 = { ⟨ 𝐴 , 𝐵 ⟩ }
Assertion	funsndifnop	⊢ ( 𝐴 ≠ 𝐵 → ¬ 𝐺 ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		funsndifnop.a	⊢ 𝐴 ∈ V
2		funsndifnop.b	⊢ 𝐵 ∈ V
3		funsndifnop.g	⊢ 𝐺 = { ⟨ 𝐴 , 𝐵 ⟩ }
4		elvv	⊢ ( 𝐺 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ )
5	1 2	funsn	⊢ Fun { ⟨ 𝐴 , 𝐵 ⟩ }
6		funeq	⊢ ( 𝐺 = { ⟨ 𝐴 , 𝐵 ⟩ } → ( Fun 𝐺 ↔ Fun { ⟨ 𝐴 , 𝐵 ⟩ } ) )
7	5 6	mpbiri	⊢ ( 𝐺 = { ⟨ 𝐴 , 𝐵 ⟩ } → Fun 𝐺 )
8	3 7	ax-mp	⊢ Fun 𝐺
9		funeq	⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( Fun 𝐺 ↔ Fun ⟨ 𝑥 , 𝑦 ⟩ ) )
10		vex	⊢ 𝑥 ∈ V
11		vex	⊢ 𝑦 ∈ V
12	10 11	funop	⊢ ( Fun ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑎 ( 𝑥 = { 𝑎 } ∧ ⟨ 𝑥 , 𝑦 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
13	9 12	bitrdi	⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( Fun 𝐺 ↔ ∃ 𝑎 ( 𝑥 = { 𝑎 } ∧ ⟨ 𝑥 , 𝑦 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
14		eqeq2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } → ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐺 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
15		eqeq1	⊢ ( 𝐺 = { ⟨ 𝐴 , 𝐵 ⟩ } → ( 𝐺 = { ⟨ 𝑎 , 𝑎 ⟩ } ↔ { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
16		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
17	16	sneqr	⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝑎 , 𝑎 ⟩ } → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑎 ⟩ )
18	1 2	opth	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑎 ⟩ ↔ ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑎 ) )
19		eqtr3	⊢ ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑎 ) → 𝐴 = 𝐵 )
20	19	a1d	⊢ ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑎 ) → ( 𝑥 = { 𝑎 } → 𝐴 = 𝐵 ) )
21	18 20	sylbi	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑎 ⟩ → ( 𝑥 = { 𝑎 } → 𝐴 = 𝐵 ) )
22	17 21	syl	⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝑎 , 𝑎 ⟩ } → ( 𝑥 = { 𝑎 } → 𝐴 = 𝐵 ) )
23	15 22	biimtrdi	⊢ ( 𝐺 = { ⟨ 𝐴 , 𝐵 ⟩ } → ( 𝐺 = { ⟨ 𝑎 , 𝑎 ⟩ } → ( 𝑥 = { 𝑎 } → 𝐴 = 𝐵 ) ) )
24	3 23	ax-mp	⊢ ( 𝐺 = { ⟨ 𝑎 , 𝑎 ⟩ } → ( 𝑥 = { 𝑎 } → 𝐴 = 𝐵 ) )
25	14 24	biimtrdi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } → ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑥 = { 𝑎 } → 𝐴 = 𝐵 ) ) )
26	25	com23	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } → ( 𝑥 = { 𝑎 } → ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐴 = 𝐵 ) ) )
27	26	impcom	⊢ ( ( 𝑥 = { 𝑎 } ∧ ⟨ 𝑥 , 𝑦 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) → ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐴 = 𝐵 ) )
28	27	exlimiv	⊢ ( ∃ 𝑎 ( 𝑥 = { 𝑎 } ∧ ⟨ 𝑥 , 𝑦 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) → ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐴 = 𝐵 ) )
29	28	com12	⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑎 ( 𝑥 = { 𝑎 } ∧ ⟨ 𝑥 , 𝑦 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) → 𝐴 = 𝐵 ) )
30	13 29	sylbid	⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( Fun 𝐺 → 𝐴 = 𝐵 ) )
31	8 30	mpi	⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐴 = 𝐵 )
32	31	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐴 = 𝐵 )
33	4 32	sylbi	⊢ ( 𝐺 ∈ ( V × V ) → 𝐴 = 𝐵 )
34	33	necon3ai	⊢ ( 𝐴 ≠ 𝐵 → ¬ 𝐺 ∈ ( V × V ) )