Metamath Proof Explorer


Theorem mapssbi

Description: Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses mapssbi.a φAV
mapssbi.b φBW
mapssbi.c φCZ
mapssbi.n φC
Assertion mapssbi φABACBC

Proof

Step Hyp Ref Expression
1 mapssbi.a φAV
2 mapssbi.b φBW
3 mapssbi.c φCZ
4 mapssbi.n φC
5 2 adantr φABBW
6 simpr φABAB
7 mapss BWABACBC
8 5 6 7 syl2anc φABACBC
9 8 ex φABACBC
10 simplr φACBC¬ABACBC
11 nssrex ¬ABxA¬xB
12 11 biimpi ¬ABxA¬xB
13 12 adantl φ¬ABxA¬xB
14 fconst6g xAC×x:CA
15 14 adantl φxAC×x:CA
16 elmapg AVCZC×xACC×x:CA
17 1 3 16 syl2anc φC×xACC×x:CA
18 17 adantr φxAC×xACC×x:CA
19 15 18 mpbird φxAC×xAC
20 19 3adant3 φxA¬xBC×xAC
21 3 adantr φC×xBCCZ
22 2 adantr φC×xBCBW
23 4 adantr φC×xBCC
24 simpr φC×xBCC×xBC
25 21 22 23 24 snelmap φC×xBCxB
26 25 adantlr φ¬xBC×xBCxB
27 simplr φ¬xBC×xBC¬xB
28 26 27 pm2.65da φ¬xB¬C×xBC
29 28 3adant2 φxA¬xB¬C×xBC
30 nelss C×xAC¬C×xBC¬ACBC
31 20 29 30 syl2anc φxA¬xB¬ACBC
32 31 3exp φxA¬xB¬ACBC
33 32 adantr φ¬ABxA¬xB¬ACBC
34 33 rexlimdv φ¬ABxA¬xB¬ACBC
35 13 34 mpd φ¬AB¬ACBC
36 35 adantlr φACBC¬AB¬ACBC
37 10 36 condan φACBCAB
38 37 ex φACBCAB
39 9 38 impbid φABACBC