Metamath Proof Explorer

Theorem paireqne

Description: Two sets are not equal iff there is exactly one proper pair whose elements are either one of these sets. (Contributed by AV, 27-Jan-2023)

Ref Expression
Hypotheses paireqne.a 
|- ( ph -> A e. V )
paireqne.b 
|- ( ph -> B e. V )
paireqne.p 
|- P = { x e. ~P V | ( # ` x ) = 2 }
Assertion paireqne 
|- ( ph -> ( E! p e. P A. x e. p ( x = A \/ x = B ) <-> A =/= B ) )

Proof

Step Hyp Ref Expression
1 paireqne.a 
 |-  ( ph -> A e. V )
2 paireqne.b 
 |-  ( ph -> B e. V )
3 paireqne.p 
 |-  P = { x e. ~P V | ( # ` x ) = 2 }
4 raleq 
 |-  ( p = q -> ( A. x e. p ( x = A \/ x = B ) <-> A. x e. q ( x = A \/ x = B ) ) )
5 4 reu8 
 |-  ( E! p e. P A. x e. p ( x = A \/ x = B ) <-> E. p e. P ( A. x e. p ( x = A \/ x = B ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) ) )
6 3 eleq2i 
 |-  ( p e. P <-> p e. { x e. ~P V | ( # ` x ) = 2 } )
7 elss2prb 
 |-  ( p e. { x e. ~P V | ( # ` x ) = 2 } <-> E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) )
8 6 7 bitri 
 |-  ( p e. P <-> E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) )
9 raleq 
 |-  ( p = { a , b } -> ( A. x e. p ( x = A \/ x = B ) <-> A. x e. { a , b } ( x = A \/ x = B ) ) )
10 vex 
 |-  a e. _V
11 vex 
 |-  b e. _V
12 eqeq1 
 |-  ( x = a -> ( x = A <-> a = A ) )
13 eqeq1 
 |-  ( x = a -> ( x = B <-> a = B ) )
14 12 13 orbi12d 
 |-  ( x = a -> ( ( x = A \/ x = B ) <-> ( a = A \/ a = B ) ) )
15 eqeq1 
 |-  ( x = b -> ( x = A <-> b = A ) )
16 eqeq1 
 |-  ( x = b -> ( x = B <-> b = B ) )
17 15 16 orbi12d 
 |-  ( x = b -> ( ( x = A \/ x = B ) <-> ( b = A \/ b = B ) ) )
18 10 11 14 17 ralpr 
 |-  ( A. x e. { a , b } ( x = A \/ x = B ) <-> ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) )
19 9 18 bitrdi 
 |-  ( p = { a , b } -> ( A. x e. p ( x = A \/ x = B ) <-> ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) )
20 eqeq1 
 |-  ( p = { a , b } -> ( p = q <-> { a , b } = q ) )
21 20 imbi2d 
 |-  ( p = { a , b } -> ( ( A. x e. q ( x = A \/ x = B ) -> p = q ) <-> ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) ) )
22 21 ralbidv 
 |-  ( p = { a , b } -> ( A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) <-> A. q e. P ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) ) )
23 19 22 anbi12d 
 |-  ( p = { a , b } -> ( ( A. x e. p ( x = A \/ x = B ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) ) <-> ( ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) ) ) )
24 23 ad2antll 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> ( ( A. x e. p ( x = A \/ x = B ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) ) <-> ( ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) ) ) )
25 1 2 jca 
 |-  ( ph -> ( A e. V /\ B e. V ) )
26 prelpwi 
 |-  ( ( A e. V /\ B e. V ) -> { A , B } e. ~P V )
27 25 26 syl 
 |-  ( ph -> { A , B } e. ~P V )
28 27 ad3antrrr 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> { A , B } e. ~P V )
29 hashprg 
 |-  ( ( a e. V /\ b e. V ) -> ( a =/= b <-> ( # ` { a , b } ) = 2 ) )
30 29 adantl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a =/= b <-> ( # ` { a , b } ) = 2 ) )
31 30 biimpd 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a =/= b -> ( # ` { a , b } ) = 2 ) )
32 31 com12 
 |-  ( a =/= b -> ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( # ` { a , b } ) = 2 ) )
33 32 adantr 
 |-  ( ( a =/= b /\ p = { a , b } ) -> ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( # ` { a , b } ) = 2 ) )
34 33 impcom 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> ( # ` { a , b } ) = 2 )
35 34 adantr 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( # ` { a , b } ) = 2 )
36 eqtr3 
 |-  ( ( b = A /\ a = A ) -> b = a )
37 eqneqall 
 |-  ( a = b -> ( a =/= b -> ( p = { a , b } -> { A , B } = { a , b } ) ) )
38 37 impd 
 |-  ( a = b -> ( ( a =/= b /\ p = { a , b } ) -> { A , B } = { a , b } ) )
39 38 a1d 
 |-  ( a = b -> ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( a =/= b /\ p = { a , b } ) -> { A , B } = { a , b } ) ) )
40 39 impd 
 |-  ( a = b -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) )
41 40 equcoms 
 |-  ( b = a -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) )
42 36 41 syl 
 |-  ( ( b = A /\ a = A ) -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) )
43 42 ex 
 |-  ( b = A -> ( a = A -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) ) )
44 preq12 
 |-  ( ( a = A /\ b = B ) -> { a , b } = { A , B } )
45 44 eqcomd 
 |-  ( ( a = A /\ b = B ) -> { A , B } = { a , b } )
46 45 a1d 
 |-  ( ( a = A /\ b = B ) -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) )
47 46 expcom 
 |-  ( b = B -> ( a = A -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) ) )
48 43 47 jaoi 
 |-  ( ( b = A \/ b = B ) -> ( a = A -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) ) )
49 48 com12 
 |-  ( a = A -> ( ( b = A \/ b = B ) -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) ) )
50 prcom 
 |-  { a , b } = { b , a }
51 preq12 
 |-  ( ( b = A /\ a = B ) -> { b , a } = { A , B } )
52 50 51 eqtrid 
 |-  ( ( b = A /\ a = B ) -> { a , b } = { A , B } )
53 52 eqcomd 
 |-  ( ( b = A /\ a = B ) -> { A , B } = { a , b } )
54 53 a1d 
 |-  ( ( b = A /\ a = B ) -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) )
55 54 ex 
 |-  ( b = A -> ( a = B -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) ) )
56 eqtr3 
 |-  ( ( b = B /\ a = B ) -> b = a )
57 56 41 syl 
 |-  ( ( b = B /\ a = B ) -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) )
58 57 ex 
 |-  ( b = B -> ( a = B -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) ) )
59 55 58 jaoi 
 |-  ( ( b = A \/ b = B ) -> ( a = B -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) ) )
60 59 com12 
 |-  ( a = B -> ( ( b = A \/ b = B ) -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) ) )
61 49 60 jaoi 
 |-  ( ( a = A \/ a = B ) -> ( ( b = A \/ b = B ) -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) ) )
62 61 imp 
 |-  ( ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) -> ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> { A , B } = { a , b } ) )
63 62 impcom 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> { A , B } = { a , b } )
64 63 fveqeq2d 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( ( # ` { A , B } ) = 2 <-> ( # ` { a , b } ) = 2 ) )
65 35 64 mpbird 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( # ` { A , B } ) = 2 )
66 28 65 jca 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( { A , B } e. ~P V /\ ( # ` { A , B } ) = 2 ) )
67 3 eleq2i 
 |-  ( { A , B } e. P <-> { A , B } e. { x e. ~P V | ( # ` x ) = 2 } )
68 fveqeq2 
 |-  ( x = { A , B } -> ( ( # ` x ) = 2 <-> ( # ` { A , B } ) = 2 ) )
69 68 elrab 
 |-  ( { A , B } e. { x e. ~P V | ( # ` x ) = 2 } <-> ( { A , B } e. ~P V /\ ( # ` { A , B } ) = 2 ) )
70 67 69 bitri 
 |-  ( { A , B } e. P <-> ( { A , B } e. ~P V /\ ( # ` { A , B } ) = 2 ) )
71 66 70 sylibr 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> { A , B } e. P )
72 raleq 
 |-  ( q = { A , B } -> ( A. x e. q ( x = A \/ x = B ) <-> A. x e. { A , B } ( x = A \/ x = B ) ) )
73 eqeq2 
 |-  ( q = { A , B } -> ( { a , b } = q <-> { a , b } = { A , B } ) )
74 72 73 imbi12d 
 |-  ( q = { A , B } -> ( ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) <-> ( A. x e. { A , B } ( x = A \/ x = B ) -> { a , b } = { A , B } ) ) )
75 74 rspcv 
 |-  ( { A , B } e. P -> ( A. q e. P ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) -> ( A. x e. { A , B } ( x = A \/ x = B ) -> { a , b } = { A , B } ) ) )
76 71 75 syl 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( A. q e. P ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) -> ( A. x e. { A , B } ( x = A \/ x = B ) -> { a , b } = { A , B } ) ) )
77 eqeq1 
 |-  ( x = A -> ( x = A <-> A = A ) )
78 eqeq1 
 |-  ( x = A -> ( x = B <-> A = B ) )
79 77 78 orbi12d 
 |-  ( x = A -> ( ( x = A \/ x = B ) <-> ( A = A \/ A = B ) ) )
80 eqeq1 
 |-  ( x = B -> ( x = A <-> B = A ) )
81 eqeq1 
 |-  ( x = B -> ( x = B <-> B = B ) )
82 80 81 orbi12d 
 |-  ( x = B -> ( ( x = A \/ x = B ) <-> ( B = A \/ B = B ) ) )
83 79 82 ralprg 
 |-  ( ( A e. V /\ B e. V ) -> ( A. x e. { A , B } ( x = A \/ x = B ) <-> ( ( A = A \/ A = B ) /\ ( B = A \/ B = B ) ) ) )
84 25 83 syl 
 |-  ( ph -> ( A. x e. { A , B } ( x = A \/ x = B ) <-> ( ( A = A \/ A = B ) /\ ( B = A \/ B = B ) ) ) )
85 84 imbi1d 
 |-  ( ph -> ( ( A. x e. { A , B } ( x = A \/ x = B ) -> { a , b } = { A , B } ) <-> ( ( ( A = A \/ A = B ) /\ ( B = A \/ B = B ) ) -> { a , b } = { A , B } ) ) )
86 85 ad3antrrr 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( ( A. x e. { A , B } ( x = A \/ x = B ) -> { a , b } = { A , B } ) <-> ( ( ( A = A \/ A = B ) /\ ( B = A \/ B = B ) ) -> { a , b } = { A , B } ) ) )
87 eqid 
 |-  A = A
88 87 orci 
 |-  ( A = A \/ A = B )
89 eqid 
 |-  B = B
90 89 olci 
 |-  ( B = A \/ B = B )
91 pm5.5 
 |-  ( ( ( A = A \/ A = B ) /\ ( B = A \/ B = B ) ) -> ( ( ( ( A = A \/ A = B ) /\ ( B = A \/ B = B ) ) -> { a , b } = { A , B } ) <-> { a , b } = { A , B } ) )
92 88 90 91 mp2an 
 |-  ( ( ( ( A = A \/ A = B ) /\ ( B = A \/ B = B ) ) -> { a , b } = { A , B } ) <-> { a , b } = { A , B } )
93 10 11 pm3.2i 
 |-  ( a e. _V /\ b e. _V )
94 preq12bg 
 |-  ( ( ( a e. _V /\ b e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( { a , b } = { A , B } <-> ( ( a = A /\ b = B ) \/ ( a = B /\ b = A ) ) ) )
95 93 25 94 sylancr 
 |-  ( ph -> ( { a , b } = { A , B } <-> ( ( a = A /\ b = B ) \/ ( a = B /\ b = A ) ) ) )
96 95 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( { a , b } = { A , B } <-> ( ( a = A /\ b = B ) \/ ( a = B /\ b = A ) ) ) )
97 96 adantr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> ( { a , b } = { A , B } <-> ( ( a = A /\ b = B ) \/ ( a = B /\ b = A ) ) ) )
98 eqeq12 
 |-  ( ( a = A /\ b = B ) -> ( a = b <-> A = B ) )
99 98 necon3bid 
 |-  ( ( a = A /\ b = B ) -> ( a =/= b <-> A =/= B ) )
100 99 biimpd 
 |-  ( ( a = A /\ b = B ) -> ( a =/= b -> A =/= B ) )
101 eqeq12 
 |-  ( ( a = B /\ b = A ) -> ( a = b <-> B = A ) )
102 101 necon3bid 
 |-  ( ( a = B /\ b = A ) -> ( a =/= b <-> B =/= A ) )
103 102 biimpd 
 |-  ( ( a = B /\ b = A ) -> ( a =/= b -> B =/= A ) )
104 necom 
 |-  ( A =/= B <-> B =/= A )
105 103 104 imbitrrdi 
 |-  ( ( a = B /\ b = A ) -> ( a =/= b -> A =/= B ) )
106 100 105 jaoi 
 |-  ( ( ( a = A /\ b = B ) \/ ( a = B /\ b = A ) ) -> ( a =/= b -> A =/= B ) )
107 106 com12 
 |-  ( a =/= b -> ( ( ( a = A /\ b = B ) \/ ( a = B /\ b = A ) ) -> A =/= B ) )
108 107 ad2antrl 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> ( ( ( a = A /\ b = B ) \/ ( a = B /\ b = A ) ) -> A =/= B ) )
109 97 108 sylbid 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> ( { a , b } = { A , B } -> A =/= B ) )
110 109 adantr 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( { a , b } = { A , B } -> A =/= B ) )
111 92 110 biimtrid 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( ( ( ( A = A \/ A = B ) /\ ( B = A \/ B = B ) ) -> { a , b } = { A , B } ) -> A =/= B ) )
112 86 111 sylbid 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( ( A. x e. { A , B } ( x = A \/ x = B ) -> { a , b } = { A , B } ) -> A =/= B ) )
113 76 112 syld 
 |-  ( ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) /\ ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) ) -> ( A. q e. P ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) -> A =/= B ) )
114 113 ex 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> ( ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) -> ( A. q e. P ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) -> A =/= B ) ) )
115 114 impd 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> ( ( ( ( a = A \/ a = B ) /\ ( b = A \/ b = B ) ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> { a , b } = q ) ) -> A =/= B ) )
116 24 115 sylbid 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ p = { a , b } ) ) -> ( ( A. x e. p ( x = A \/ x = B ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) ) -> A =/= B ) )
117 116 ex 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( a =/= b /\ p = { a , b } ) -> ( ( A. x e. p ( x = A \/ x = B ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) ) -> A =/= B ) ) )
118 117 rexlimdvva 
 |-  ( ph -> ( E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) -> ( ( A. x e. p ( x = A \/ x = B ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) ) -> A =/= B ) ) )
119 8 118 biimtrid 
 |-  ( ph -> ( p e. P -> ( ( A. x e. p ( x = A \/ x = B ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) ) -> A =/= B ) ) )
120 119 imp 
 |-  ( ( ph /\ p e. P ) -> ( ( A. x e. p ( x = A \/ x = B ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) ) -> A =/= B ) )
121 120 rexlimdva 
 |-  ( ph -> ( E. p e. P ( A. x e. p ( x = A \/ x = B ) /\ A. q e. P ( A. x e. q ( x = A \/ x = B ) -> p = q ) ) -> A =/= B ) )
122 5 121 biimtrid 
 |-  ( ph -> ( E! p e. P A. x e. p ( x = A \/ x = B ) -> A =/= B ) )
123 27 adantr 
 |-  ( ( ph /\ A =/= B ) -> { A , B } e. ~P V )
124 hashprg 
 |-  ( ( A e. V /\ B e. V ) -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )
125 25 124 syl 
 |-  ( ph -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )
126 125 biimpd 
 |-  ( ph -> ( A =/= B -> ( # ` { A , B } ) = 2 ) )
127 126 imp 
 |-  ( ( ph /\ A =/= B ) -> ( # ` { A , B } ) = 2 )
128 123 127 jca 
 |-  ( ( ph /\ A =/= B ) -> ( { A , B } e. ~P V /\ ( # ` { A , B } ) = 2 ) )
129 128 70 sylibr 
 |-  ( ( ph /\ A =/= B ) -> { A , B } e. P )
130 raleq 
 |-  ( p = { A , B } -> ( A. x e. p ( x = A \/ x = B ) <-> A. x e. { A , B } ( x = A \/ x = B ) ) )
131 eqeq1 
 |-  ( p = { A , B } -> ( p = y <-> { A , B } = y ) )
132 131 imbi2d 
 |-  ( p = { A , B } -> ( ( A. x e. y ( x = A \/ x = B ) -> p = y ) <-> ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) ) )
133 132 ralbidv 
 |-  ( p = { A , B } -> ( A. y e. P ( A. x e. y ( x = A \/ x = B ) -> p = y ) <-> A. y e. P ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) ) )
134 130 133 anbi12d 
 |-  ( p = { A , B } -> ( ( A. x e. p ( x = A \/ x = B ) /\ A. y e. P ( A. x e. y ( x = A \/ x = B ) -> p = y ) ) <-> ( A. x e. { A , B } ( x = A \/ x = B ) /\ A. y e. P ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) ) ) )
135 134 adantl 
 |-  ( ( ( ph /\ A =/= B ) /\ p = { A , B } ) -> ( ( A. x e. p ( x = A \/ x = B ) /\ A. y e. P ( A. x e. y ( x = A \/ x = B ) -> p = y ) ) <-> ( A. x e. { A , B } ( x = A \/ x = B ) /\ A. y e. P ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) ) ) )
136 vex 
 |-  x e. _V
137 136 elpr 
 |-  ( x e. { A , B } <-> ( x = A \/ x = B ) )
138 137 a1i 
 |-  ( ( ph /\ A =/= B ) -> ( x e. { A , B } <-> ( x = A \/ x = B ) ) )
139 138 biimpd 
 |-  ( ( ph /\ A =/= B ) -> ( x e. { A , B } -> ( x = A \/ x = B ) ) )
140 139 imp 
 |-  ( ( ( ph /\ A =/= B ) /\ x e. { A , B } ) -> ( x = A \/ x = B ) )
141 140 ralrimiva 
 |-  ( ( ph /\ A =/= B ) -> A. x e. { A , B } ( x = A \/ x = B ) )
142 3 eleq2i 
 |-  ( y e. P <-> y e. { x e. ~P V | ( # ` x ) = 2 } )
143 elss2prb 
 |-  ( y e. { x e. ~P V | ( # ` x ) = 2 } <-> E. a e. V E. b e. V ( a =/= b /\ y = { a , b } ) )
144 142 143 bitri 
 |-  ( y e. P <-> E. a e. V E. b e. V ( a =/= b /\ y = { a , b } ) )
145 prid1g 
 |-  ( a e. V -> a e. { a , b } )
146 145 ad2antrl 
 |-  ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) -> a e. { a , b } )
147 146 adantr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> a e. { a , b } )
148 eleq2 
 |-  ( y = { a , b } -> ( a e. y <-> a e. { a , b } ) )
149 148 ad2antll 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> ( a e. y <-> a e. { a , b } ) )
150 147 149 mpbird 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> a e. y )
151 14 rspcv 
 |-  ( a e. y -> ( A. x e. y ( x = A \/ x = B ) -> ( a = A \/ a = B ) ) )
152 150 151 syl 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> ( A. x e. y ( x = A \/ x = B ) -> ( a = A \/ a = B ) ) )
153 prid2g 
 |-  ( b e. V -> b e. { a , b } )
154 153 ad2antll 
 |-  ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) -> b e. { a , b } )
155 154 adantr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> b e. { a , b } )
156 eleq2 
 |-  ( y = { a , b } -> ( b e. y <-> b e. { a , b } ) )
157 156 ad2antll 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> ( b e. y <-> b e. { a , b } ) )
158 155 157 mpbird 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> b e. y )
159 17 rspcv 
 |-  ( b e. y -> ( A. x e. y ( x = A \/ x = B ) -> ( b = A \/ b = B ) ) )
160 158 159 syl 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> ( A. x e. y ( x = A \/ x = B ) -> ( b = A \/ b = B ) ) )
161 simplrr 
 |-  ( ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) /\ ( ( b = A \/ b = B ) /\ ( a = A \/ a = B ) ) ) -> y = { a , b } )
162 eqtr3 
 |-  ( ( a = A /\ b = A ) -> a = b )
163 eqneqall 
 |-  ( a = b -> ( a =/= b -> { a , b } = { A , B } ) )
164 163 com12 
 |-  ( a =/= b -> ( a = b -> { a , b } = { A , B } ) )
165 164 ad2antrl 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> ( a = b -> { a , b } = { A , B } ) )
166 165 com12 
 |-  ( a = b -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) )
167 162 166 syl 
 |-  ( ( a = A /\ b = A ) -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) )
168 167 ex 
 |-  ( a = A -> ( b = A -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) ) )
169 52 a1d 
 |-  ( ( b = A /\ a = B ) -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) )
170 169 expcom 
 |-  ( a = B -> ( b = A -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) ) )
171 168 170 jaoi 
 |-  ( ( a = A \/ a = B ) -> ( b = A -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) ) )
172 171 com12 
 |-  ( b = A -> ( ( a = A \/ a = B ) -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) ) )
173 44 a1d 
 |-  ( ( a = A /\ b = B ) -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) )
174 173 ex 
 |-  ( a = A -> ( b = B -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) ) )
175 eqtr3 
 |-  ( ( a = B /\ b = B ) -> a = b )
176 175 166 syl 
 |-  ( ( a = B /\ b = B ) -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) )
177 176 ex 
 |-  ( a = B -> ( b = B -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) ) )
178 174 177 jaoi 
 |-  ( ( a = A \/ a = B ) -> ( b = B -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) ) )
179 178 com12 
 |-  ( b = B -> ( ( a = A \/ a = B ) -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) ) )
180 172 179 jaoi 
 |-  ( ( b = A \/ b = B ) -> ( ( a = A \/ a = B ) -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) ) )
181 180 imp 
 |-  ( ( ( b = A \/ b = B ) /\ ( a = A \/ a = B ) ) -> ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> { a , b } = { A , B } ) )
182 181 impcom 
 |-  ( ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) /\ ( ( b = A \/ b = B ) /\ ( a = A \/ a = B ) ) ) -> { a , b } = { A , B } )
183 161 182 eqtr2d 
 |-  ( ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) /\ ( ( b = A \/ b = B ) /\ ( a = A \/ a = B ) ) ) -> { A , B } = y )
184 183 exp32 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> ( ( b = A \/ b = B ) -> ( ( a = A \/ a = B ) -> { A , B } = y ) ) )
185 160 184 syld 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> ( A. x e. y ( x = A \/ x = B ) -> ( ( a = A \/ a = B ) -> { A , B } = y ) ) )
186 152 185 mpdd 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ y = { a , b } ) ) -> ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) )
187 186 ex 
 |-  ( ( ( ph /\ A =/= B ) /\ ( a e. V /\ b e. V ) ) -> ( ( a =/= b /\ y = { a , b } ) -> ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) ) )
188 187 rexlimdvva 
 |-  ( ( ph /\ A =/= B ) -> ( E. a e. V E. b e. V ( a =/= b /\ y = { a , b } ) -> ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) ) )
189 144 188 biimtrid 
 |-  ( ( ph /\ A =/= B ) -> ( y e. P -> ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) ) )
190 189 imp 
 |-  ( ( ( ph /\ A =/= B ) /\ y e. P ) -> ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) )
191 190 ralrimiva 
 |-  ( ( ph /\ A =/= B ) -> A. y e. P ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) )
192 141 191 jca 
 |-  ( ( ph /\ A =/= B ) -> ( A. x e. { A , B } ( x = A \/ x = B ) /\ A. y e. P ( A. x e. y ( x = A \/ x = B ) -> { A , B } = y ) ) )
193 129 135 192 rspcedvd 
 |-  ( ( ph /\ A =/= B ) -> E. p e. P ( A. x e. p ( x = A \/ x = B ) /\ A. y e. P ( A. x e. y ( x = A \/ x = B ) -> p = y ) ) )
194 raleq 
 |-  ( p = y -> ( A. x e. p ( x = A \/ x = B ) <-> A. x e. y ( x = A \/ x = B ) ) )
195 194 reu8 
 |-  ( E! p e. P A. x e. p ( x = A \/ x = B ) <-> E. p e. P ( A. x e. p ( x = A \/ x = B ) /\ A. y e. P ( A. x e. y ( x = A \/ x = B ) -> p = y ) ) )
196 193 195 sylibr 
 |-  ( ( ph /\ A =/= B ) -> E! p e. P A. x e. p ( x = A \/ x = B ) )
197 196 ex 
 |-  ( ph -> ( A =/= B -> E! p e. P A. x e. p ( x = A \/ x = B ) ) )
198 122 197 impbid 
 |-  ( ph -> ( E! p e. P A. x e. p ( x = A \/ x = B ) <-> A =/= B ) )