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) Remove antecedent. (Revised by Eric Schmidt, 9-May-2026) (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 
|- ( 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 2 3 opnzi 
 |-  <. C , D >. =/= (/)
5 4 a1i 
 |-  ( A = (/) -> <. C , D >. =/= (/) )
6 iuneq1 
 |-  ( A = (/) -> U_ x e. A { <. x , B >. } = U_ x e. (/) { <. x , B >. } )
7 0iun 
 |-  U_ x e. (/) { <. x , B >. } = (/)
8 6 7 eqtrdi 
 |-  ( A = (/) -> U_ x e. A { <. x , B >. } = (/) )
9 5 8 neeqtrrd 
 |-  ( A = (/) -> <. C , D >. =/= U_ x e. A { <. x , B >. } )
10 nesym 
 |-  ( <. C , D >. =/= U_ x e. A { <. x , B >. } <-> -. U_ x e. A { <. x , B >. } = <. C , D >. )
11 9 10 sylib 
 |-  ( A = (/) -> -. U_ x e. A { <. x , B >. } = <. C , D >. )
12 11 pm2.21d 
 |-  ( A = (/) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
13 n0snor2el 
 |-  ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )
14 nfiu1 
 |-  F/_ x U_ x e. A { <. x , B >. }
15 14 nfeq1 
 |-  F/ x U_ x e. A { <. x , B >. } = <. C , D >.
16 nfv 
 |-  F/ x E. z A = { z }
17 15 16 nfim 
 |-  F/ x ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } )
18 ssiun2 
 |-  ( x e. A -> { <. x , B >. } C_ U_ x e. A { <. x , B >. } )
19 nfcv 
 |-  F/_ x y
20 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
21 19 20 nfop 
 |-  F/_ x <. y , [_ y / x ]_ B >.
22 21 nfsn 
 |-  F/_ x { <. y , [_ y / x ]_ B >. }
23 22 14 nfss 
 |-  F/ x { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. }
24 id 
 |-  ( x = y -> x = y )
25 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
26 24 25 opeq12d 
 |-  ( x = y -> <. x , B >. = <. y , [_ y / x ]_ B >. )
27 26 sneqd 
 |-  ( x = y -> { <. x , B >. } = { <. y , [_ y / x ]_ B >. } )
28 27 sseq1d 
 |-  ( x = y -> ( { <. x , B >. } C_ U_ x e. A { <. x , B >. } <-> { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } ) )
29 19 23 28 18 vtoclgaf 
 |-  ( y e. A -> { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } )
30 18 29 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 >. } ) )
31 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 >. } )
32 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 >. ) )
33 df-pr 
 |-  { <. x , B >. , <. y , [_ y / x ]_ B >. } = ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } )
34 33 eqcomi 
 |-  ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) = { <. x , B >. , <. y , [_ y / x ]_ B >. }
35 34 sseq1i 
 |-  ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ <. C , D >. <-> { <. x , B >. , <. y , [_ y / x ]_ B >. } C_ <. C , D >. )
36 vex 
 |-  x e. _V
37 vex 
 |-  y e. _V
38 1 csbex 
 |-  [_ y / x ]_ B e. _V
39 36 1 37 38 2 3 propssopi 
 |-  ( { <. x , B >. , <. y , [_ y / x ]_ B >. } C_ <. C , D >. -> x = y )
40 eqneqall 
 |-  ( x = y -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) )
41 39 40 syl 
 |-  ( { <. x , B >. , <. y , [_ y / x ]_ B >. } C_ <. C , D >. -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) )
42 35 41 sylbi 
 |-  ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ <. C , D >. -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) )
43 32 42 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 } ) ) ) )
44 43 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 } ) ) ) )
45 31 44 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 } ) ) ) )
46 30 45 mpd 
 |-  ( ( x e. A /\ y e. A ) -> ( x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) )
47 46 rexlimdva 
 |-  ( x e. A -> ( E. y e. A x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) )
48 17 47 rexlimi 
 |-  ( E. x e. A E. y e. A x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
49 ax-1 
 |-  ( E. z A = { z } -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
50 48 49 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 } ) )
51 13 50 syl 
 |-  ( A =/= (/) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
52 12 51 pm2.61ine 
 |-  ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } )