Metamath Proof Explorer


Theorem fsetprcnexALT

Description: First version of proof for fsetprcnex , which was much more complicated. (Contributed by AV, 14-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fsetprcnexALT AVABVf|f:ABV

Proof

Step Hyp Ref Expression
1 abanssl f|f:ABbBzAfz=bf|f:AB
2 n0 AyyA
3 vex yV
4 3 a1i yAAVyV
5 fsetsnprcnex yVBVf|f:yBV
6 4 5 sylan yAAVBVf|f:yBV
7 df-nel f|f:yBV¬f|f:yBV
8 6 7 sylib yAAVBV¬f|f:yBV
9 eqid f|f:ABbBzAfz=b=f|f:ABbBzAfz=b
10 eqid f|f:yB=f|f:yB
11 eqid gf|f:yBaAgy=gf|f:yBaAgy
12 9 10 11 cfsetsnfsetf1o AVyAgf|f:yBaAgy:f|f:yB1-1 ontof|f:ABbBzAfz=b
13 12 ancoms yAAVgf|f:yBaAgy:f|f:yB1-1 ontof|f:ABbBzAfz=b
14 13 adantr yAAVBVgf|f:yBaAgy:f|f:yB1-1 ontof|f:ABbBzAfz=b
15 f1ovv gf|f:yBaAgy:f|f:yB1-1 ontof|f:ABbBzAfz=bf|f:yBVf|f:ABbBzAfz=bV
16 15 bicomd gf|f:yBaAgy:f|f:yB1-1 ontof|f:ABbBzAfz=bf|f:ABbBzAfz=bVf|f:yBV
17 14 16 syl yAAVBVf|f:ABbBzAfz=bVf|f:yBV
18 8 17 mtbird yAAVBV¬f|f:ABbBzAfz=bV
19 18 exp31 yAAVBV¬f|f:ABbBzAfz=bV
20 19 exlimiv yyAAVBV¬f|f:ABbBzAfz=bV
21 2 20 sylbi AAVBV¬f|f:ABbBzAfz=bV
22 21 impcom AVABV¬f|f:ABbBzAfz=bV
23 22 imp AVABV¬f|f:ABbBzAfz=bV
24 df-nel f|f:ABbBzAfz=bV¬f|f:ABbBzAfz=bV
25 23 24 sylibr AVABVf|f:ABbBzAfz=bV
26 prcssprc f|f:ABbBzAfz=bf|f:ABf|f:ABbBzAfz=bVf|f:ABV
27 1 25 26 sylancr AVABVf|f:ABV