Step | Hyp | Ref
| Expression |
1 | | 1st2ndb 8014 |
. . . . . . . . 9
ā¢ (š§ ā (V Ć V) ā
š§ = āØ(1st
āš§), (2nd
āš§)ā©) |
2 | 1 | biimpi 215 |
. . . . . . . 8
ā¢ (š§ ā (V Ć V) ā
š§ = āØ(1st
āš§), (2nd
āš§)ā©) |
3 | 2 | ad2antrl 726 |
. . . . . . 7
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā š§ = āØ(1st āš§), (2nd āš§)ā©) |
4 | | fvex 6904 |
. . . . . . . . . . . 12
ā¢
(1st āš§) ā V |
5 | 4 | elsn 4643 |
. . . . . . . . . . 11
ā¢
((1st āš§) ā {š} ā (1st āš§) = š) |
6 | 5 | biimpi 215 |
. . . . . . . . . 10
ā¢
((1st āš§) ā {š} ā (1st āš§) = š) |
7 | 6 | ad2antrl 726 |
. . . . . . . . 9
ā¢ ((š§ ā (V Ć V) ā§
((1st āš§)
ā {š} ā§
(2nd āš§)
ā (š“ ā {š}))) ā (1st
āš§) = š) |
8 | 7 | adantl 482 |
. . . . . . . 8
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā (1st āš§) = š) |
9 | 8 | opeq1d 4879 |
. . . . . . 7
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā āØ(1st
āš§), (2nd
āš§)ā© =
āØš, (2nd
āš§)ā©) |
10 | 3, 9 | eqtrd 2772 |
. . . . . 6
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā š§ = āØš, (2nd āš§)ā©) |
11 | | simplr 767 |
. . . . . . 7
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā š ā š) |
12 | | simprrr 780 |
. . . . . . 7
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā (2nd āš§) ā (š“ ā {š})) |
13 | | elimasng 6087 |
. . . . . . . 8
ā¢ ((š ā š ā§ (2nd āš§) ā (š“ ā {š})) ā ((2nd āš§) ā (š“ ā {š}) ā āØš, (2nd āš§)ā© ā š“)) |
14 | 13 | biimpa 477 |
. . . . . . 7
ā¢ (((š ā š ā§ (2nd āš§) ā (š“ ā {š})) ā§ (2nd āš§) ā (š“ ā {š})) ā āØš, (2nd āš§)ā© ā š“) |
15 | 11, 12, 12, 14 | syl21anc 836 |
. . . . . 6
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā āØš, (2nd āš§)ā© ā š“) |
16 | 10, 15 | eqeltrd 2833 |
. . . . 5
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā š§ ā š“) |
17 | | fvres 6910 |
. . . . . . 7
ā¢ (š§ ā š“ ā ((1st ā¾ š“)āš§) = (1st āš§)) |
18 | 16, 17 | syl 17 |
. . . . . 6
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā ((1st ā¾ š“)āš§) = (1st āš§)) |
19 | 18, 8 | eqtrd 2772 |
. . . . 5
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā ((1st ā¾ š“)āš§) = š) |
20 | 16, 19 | jca 512 |
. . . 4
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) ā (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) |
21 | | df-rel 5683 |
. . . . . . . . 9
ā¢ (Rel
š“ ā š“ ā (V Ć V)) |
22 | 21 | biimpi 215 |
. . . . . . . 8
ā¢ (Rel
š“ ā š“ ā (V Ć V)) |
23 | 22 | adantr 481 |
. . . . . . 7
ā¢ ((Rel
š“ ā§ š ā š) ā š“ ā (V Ć V)) |
24 | 23 | sselda 3982 |
. . . . . 6
ā¢ (((Rel
š“ ā§ š ā š) ā§ š§ ā š“) ā š§ ā (V Ć V)) |
25 | 24 | adantrr 715 |
. . . . 5
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā š§ ā (V Ć V)) |
26 | 17 | ad2antrl 726 |
. . . . . . . 8
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā ((1st ā¾ š“)āš§) = (1st āš§)) |
27 | | simprr 771 |
. . . . . . . 8
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā ((1st ā¾ š“)āš§) = š) |
28 | 26, 27 | eqtr3d 2774 |
. . . . . . 7
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā (1st āš§) = š) |
29 | 28, 5 | sylibr 233 |
. . . . . 6
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā (1st āš§) ā {š}) |
30 | 28, 29 | eqeltrrd 2834 |
. . . . . . . . 9
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā š ā {š}) |
31 | | simpr 485 |
. . . . . . . . . . 11
ā¢ ((((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā§ š„ = š) ā š„ = š) |
32 | 31 | opeq1d 4879 |
. . . . . . . . . 10
ā¢ ((((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā§ š„ = š) ā āØš„, (2nd āš§)ā© = āØš, (2nd āš§)ā©) |
33 | 32 | eleq1d 2818 |
. . . . . . . . 9
ā¢ ((((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā§ š„ = š) ā (āØš„, (2nd āš§)ā© ā š“ ā āØš, (2nd āš§)ā© ā š“)) |
34 | | 1st2nd 8024 |
. . . . . . . . . . . 12
ā¢ ((Rel
š“ ā§ š§ ā š“) ā š§ = āØ(1st āš§), (2nd āš§)ā©) |
35 | 34 | ad2ant2r 745 |
. . . . . . . . . . 11
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā š§ = āØ(1st āš§), (2nd āš§)ā©) |
36 | 28 | opeq1d 4879 |
. . . . . . . . . . 11
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā āØ(1st āš§), (2nd āš§)ā© = āØš, (2nd āš§)ā©) |
37 | 35, 36 | eqtrd 2772 |
. . . . . . . . . 10
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā š§ = āØš, (2nd āš§)ā©) |
38 | | simprl 769 |
. . . . . . . . . 10
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā š§ ā š“) |
39 | 37, 38 | eqeltrrd 2834 |
. . . . . . . . 9
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā āØš, (2nd āš§)ā© ā š“) |
40 | 30, 33, 39 | rspcedvd 3614 |
. . . . . . . 8
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā āš„ ā {š}āØš„, (2nd āš§)ā© ā š“) |
41 | | df-rex 3071 |
. . . . . . . 8
ā¢
(āš„ ā
{š}āØš„, (2nd āš§)ā© ā š“ ā āš„(š„ ā {š} ā§ āØš„, (2nd āš§)ā© ā š“)) |
42 | 40, 41 | sylib 217 |
. . . . . . 7
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā āš„(š„ ā {š} ā§ āØš„, (2nd āš§)ā© ā š“)) |
43 | | fvex 6904 |
. . . . . . . 8
ā¢
(2nd āš§) ā V |
44 | 43 | elima3 6066 |
. . . . . . 7
ā¢
((2nd āš§) ā (š“ ā {š}) ā āš„(š„ ā {š} ā§ āØš„, (2nd āš§)ā© ā š“)) |
45 | 42, 44 | sylibr 233 |
. . . . . 6
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā (2nd āš§) ā (š“ ā {š})) |
46 | 29, 45 | jca 512 |
. . . . 5
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā ((1st āš§) ā {š} ā§ (2nd āš§) ā (š“ ā {š}))) |
47 | 25, 46 | jca 512 |
. . . 4
ā¢ (((Rel
š“ ā§ š ā š) ā§ (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) ā (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) |
48 | 20, 47 | impbida 799 |
. . 3
ā¢ ((Rel
š“ ā§ š ā š) ā ((š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š}))) ā (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š))) |
49 | | elxp7 8009 |
. . . 4
ā¢ (š§ ā ({š} Ć (š“ ā {š})) ā (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š})))) |
50 | 49 | a1i 11 |
. . 3
ā¢ ((Rel
š“ ā§ š ā š) ā (š§ ā ({š} Ć (š“ ā {š})) ā (š§ ā (V Ć V) ā§ ((1st
āš§) ā {š} ā§ (2nd
āš§) ā (š“ ā {š}))))) |
51 | | fo1st 7994 |
. . . . . . 7
ā¢
1st :VāontoāV |
52 | | fofn 6807 |
. . . . . . 7
ā¢
(1st :VāontoāV ā 1st Fn V) |
53 | 51, 52 | ax-mp 5 |
. . . . . 6
ā¢
1st Fn V |
54 | | ssv 4006 |
. . . . . 6
ā¢ š“ ā V |
55 | | fnssres 6673 |
. . . . . 6
ā¢
((1st Fn V ā§ š“ ā V) ā (1st ā¾
š“) Fn š“) |
56 | 53, 54, 55 | mp2an 690 |
. . . . 5
ā¢
(1st ā¾ š“) Fn š“ |
57 | | fniniseg 7061 |
. . . . 5
ā¢
((1st ā¾ š“) Fn š“ ā (š§ ā (ā”(1st ā¾ š“) ā {š}) ā (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š))) |
58 | 56, 57 | ax-mp 5 |
. . . 4
ā¢ (š§ ā (ā”(1st ā¾ š“) ā {š}) ā (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š)) |
59 | 58 | a1i 11 |
. . 3
ā¢ ((Rel
š“ ā§ š ā š) ā (š§ ā (ā”(1st ā¾ š“) ā {š}) ā (š§ ā š“ ā§ ((1st ā¾ š“)āš§) = š))) |
60 | 48, 50, 59 | 3bitr4rd 311 |
. 2
ā¢ ((Rel
š“ ā§ š ā š) ā (š§ ā (ā”(1st ā¾ š“) ā {š}) ā š§ ā ({š} Ć (š“ ā {š})))) |
61 | 60 | eqrdv 2730 |
1
ā¢ ((Rel
š“ ā§ š ā š) ā (ā”(1st ā¾ š“) ā {š}) = ({š} Ć (š“ ā {š}))) |