Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  hashdifpr Unicode version

Theorem hashdifpr 10559
 Description: The size of the difference of a finite set and a proper ordered pair subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.)
Assertion
Ref Expression
hashdifpr

Proof of Theorem hashdifpr
StepHypRef Expression
1 difpr 3657 . . . 4
21a1i 9 . . 3
32fveq2d 5418 . 2
4 simpl 108 . . . 4
5 snfig 6701 . . . . . 6
653ad2ant1 1002 . . . . 5
76adantl 275 . . . 4
8 snssi 3659 . . . . . 6
983ad2ant1 1002 . . . . 5
109adantl 275 . . . 4
11 diffifi 6781 . . . 4
124, 7, 10, 11syl3anc 1216 . . 3
13 simpr2 988 . . . 4
14 simpr3 989 . . . . 5
1514necomd 2392 . . . 4
16 eldifsn 3645 . . . 4
1713, 15, 16sylanbrc 413 . . 3
18 hashdifsn 10558 . . 3
1912, 17, 18syl2anc 408 . 2
20 hashdifsn 10558 . . . . 5
21203ad2antr1 1146 . . . 4
2221oveq1d 5782 . . 3
23 hashcl 10520 . . . . . 6
2423nn0cnd 9025 . . . . 5
25 sub1m1 8963 . . . . 5
2624, 25syl 14 . . . 4