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	\|- A e. _V
	funsndifnop.b	\|- B e. _V
	funsndifnop.g	\|- G = { <. A , B >. }
Assertion	funsndifnop	\|- ( A =/= B -> -. G e. ( _V X. _V ) )

Proof

Step	Hyp	Ref	Expression
1		funsndifnop.a	\|- A e. _V
2		funsndifnop.b	\|- B e. _V
3		funsndifnop.g	\|- G = { <. A , B >. }
4		elvv	\|- ( G e. ( _V X. _V ) <-> E. x E. y G = <. x , y >. )
5	1 2	funsn	\|- Fun { <. A , B >. }
6		funeq	\|- ( G = { <. A , B >. } -> ( Fun G <-> Fun { <. A , B >. } ) )
7	5 6	mpbiri	\|- ( G = { <. A , B >. } -> Fun G )
8	3 7	ax-mp	\|- Fun G
9		funeq	\|- ( G = <. x , y >. -> ( Fun G <-> Fun <. x , y >. ) )
10		vex	\|- x e. _V
11		vex	\|- y e. _V
12	10 11	funop	\|- ( Fun <. x , y >. <-> E. a ( x = { a } /\ <. x , y >. = { <. a , a >. } ) )
13	9 12	bitrdi	\|- ( G = <. x , y >. -> ( Fun G <-> E. a ( x = { a } /\ <. x , y >. = { <. a , a >. } ) ) )
14		eqeq2	\|- ( <. x , y >. = { <. a , a >. } -> ( G = <. x , y >. <-> G = { <. a , a >. } ) )
15		eqeq1	\|- ( G = { <. A , B >. } -> ( G = { <. a , a >. } <-> { <. A , B >. } = { <. a , a >. } ) )
16		opex	\|- <. A , B >. e. _V
17	16	sneqr	\|- ( { <. A , B >. } = { <. a , a >. } -> <. A , B >. = <. a , a >. )
18	1 2	opth	\|- ( <. A , B >. = <. a , a >. <-> ( A = a /\ B = a ) )
19		eqtr3	\|- ( ( A = a /\ B = a ) -> A = B )
20	19	a1d	\|- ( ( A = a /\ B = a ) -> ( x = { a } -> A = B ) )
21	18 20	sylbi	\|- ( <. A , B >. = <. a , a >. -> ( x = { a } -> A = B ) )
22	17 21	syl	\|- ( { <. A , B >. } = { <. a , a >. } -> ( x = { a } -> A = B ) )
23	15 22	biimtrdi	\|- ( G = { <. A , B >. } -> ( G = { <. a , a >. } -> ( x = { a } -> A = B ) ) )
24	3 23	ax-mp	\|- ( G = { <. a , a >. } -> ( x = { a } -> A = B ) )
25	14 24	biimtrdi	\|- ( <. x , y >. = { <. a , a >. } -> ( G = <. x , y >. -> ( x = { a } -> A = B ) ) )
26	25	com23	\|- ( <. x , y >. = { <. a , a >. } -> ( x = { a } -> ( G = <. x , y >. -> A = B ) ) )
27	26	impcom	\|- ( ( x = { a } /\ <. x , y >. = { <. a , a >. } ) -> ( G = <. x , y >. -> A = B ) )
28	27	exlimiv	\|- ( E. a ( x = { a } /\ <. x , y >. = { <. a , a >. } ) -> ( G = <. x , y >. -> A = B ) )
29	28	com12	\|- ( G = <. x , y >. -> ( E. a ( x = { a } /\ <. x , y >. = { <. a , a >. } ) -> A = B ) )
30	13 29	sylbid	\|- ( G = <. x , y >. -> ( Fun G -> A = B ) )
31	8 30	mpi	\|- ( G = <. x , y >. -> A = B )
32	31	exlimivv	\|- ( E. x E. y G = <. x , y >. -> A = B )
33	4 32	sylbi	\|- ( G e. ( _V X. _V ) -> A = B )
34	33	necon3ai	\|- ( A =/= B -> -. G e. ( _V X. _V ) )

Metamath Proof Explorer

Theorem funsndifnop

Proof