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
|
syl5eq |
|- ( ( 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
|
syl6ibr |
|- ( ( 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
|
syl5bi |
|- ( ( ( ( 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
|
syl5bi |
|- ( 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
|
syl5bi |
|- ( 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
|
syl5bi |
|- ( ( 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 ) ) |