Metamath Proof Explorer

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 
|- B e. _V
iunopeqop.c 
|- C e. _V
iunopeqop.d 
|- D e. _V
Assertion iunopeqop 
|- ( A =/= (/) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )

Proof

Step Hyp Ref Expression
1 iunopeqop.b 
 |-  B e. _V
2 iunopeqop.c 
 |-  C e. _V
3 iunopeqop.d 
 |-  D e. _V
4 n0snor2el 
 |-  ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )
5 nfiu1 
 |-  F/_ x U_ x e. A { <. x , B >. }
6 5 nfeq1 
 |-  F/ x U_ x e. A { <. x , B >. } = <. C , D >.
7 nfv 
 |-  F/ x E. z A = { z }
8 6 7 nfim 
 |-  F/ x ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } )
9 ssiun2 
 |-  ( x e. A -> { <. x , B >. } C_ U_ x e. A { <. x , B >. } )
10 nfcv 
 |-  F/_ x y
11 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
12 10 11 nfop 
 |-  F/_ x <. y , [_ y / x ]_ B >.
13 12 nfsn 
 |-  F/_ x { <. y , [_ y / x ]_ B >. }
14 13 5 nfss 
 |-  F/ x { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. }
15 id 
 |-  ( x = y -> x = y )
16 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
17 15 16 opeq12d 
 |-  ( x = y -> <. x , B >. = <. y , [_ y / x ]_ B >. )
18 17 sneqd 
 |-  ( x = y -> { <. x , B >. } = { <. y , [_ y / x ]_ B >. } )
19 18 sseq1d 
 |-  ( x = y -> ( { <. x , B >. } C_ U_ x e. A { <. x , B >. } <-> { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } ) )
20 10 14 19 9 vtoclgaf 
 |-  ( y e. A -> { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } )
21 9 20 anim12i 
 |-  ( ( x e. A /\ y e. A ) -> ( { <. x , B >. } C_ U_ x e. A { <. x , B >. } /\ { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } ) )
22 unss 
 |-  ( ( { <. x , B >. } C_ U_ x e. A { <. x , B >. } /\ { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } ) <-> ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ U_ x e. A { <. x , B >. } )
23 sseq2 
 |-  ( U_ x e. A { <. x , B >. } = <. C , D >. -> ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ U_ x e. A { <. x , B >. } <-> ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ <. C , D >. ) )
24 df-pr 
 |-  { <. x , B >. , <. y , [_ y / x ]_ B >. } = ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } )
25 24 eqcomi 
 |-  ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) = { <. x , B >. , <. y , [_ y / x ]_ B >. }
26 25 sseq1i 
 |-  ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ <. C , D >. <-> { <. x , B >. , <. y , [_ y / x ]_ B >. } C_ <. C , D >. )
27 vex 
 |-  x e. _V
28 vex 
 |-  y e. _V
29 1 csbex 
 |-  [_ y / x ]_ B e. _V
30 27 1 28 29 2 3 propssopi 
 |-  ( { <. x , B >. , <. y , [_ y / x ]_ B >. } C_ <. C , D >. -> x = y )
31 eqneqall 
 |-  ( x = y -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) )
32 30 31 syl 
 |-  ( { <. x , B >. , <. y , [_ y / x ]_ B >. } C_ <. C , D >. -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) )
33 26 32 sylbi 
 |-  ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ <. C , D >. -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) )
34 23 33 biimtrdi 
 |-  ( U_ x e. A { <. x , B >. } = <. C , D >. -> ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ U_ x e. A { <. x , B >. } -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) ) )
35 34 com14 
 |-  ( ( x e. A /\ y e. A ) -> ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ U_ x e. A { <. x , B >. } -> ( x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) ) )
36 22 35 biimtrid 
 |-  ( ( x e. A /\ y e. A ) -> ( ( { <. x , B >. } C_ U_ x e. A { <. x , B >. } /\ { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } ) -> ( x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) ) )
37 21 36 mpd 
 |-  ( ( x e. A /\ y e. A ) -> ( x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) )
38 37 rexlimdva 
 |-  ( x e. A -> ( E. y e. A x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) )
39 8 38 rexlimi 
 |-  ( E. x e. A E. y e. A x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
40 ax-1 
 |-  ( E. z A = { z } -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
41 39 40 jaoi 
 |-  ( ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
42 4 41 syl 
 |-  ( A =/= (/) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )