Metamath Proof Explorer


Theorem supisolem

Description: Lemma for supiso . (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supiso.1 φ F Isom R , S A B
supiso.2 φ C A
Assertion supisolem φ D A y C ¬ D R y y A y R D z C y R z w F C ¬ F D S w w B w S F D v F C w S v

Proof

Step Hyp Ref Expression
1 supiso.1 φ F Isom R , S A B
2 supiso.2 φ C A
3 1 2 jca φ F Isom R , S A B C A
4 simpll F Isom R , S A B C A D A F Isom R , S A B
5 4 adantr F Isom R , S A B C A D A y C F Isom R , S A B
6 simplr F Isom R , S A B C A D A y C D A
7 simplr F Isom R , S A B C A D A C A
8 7 sselda F Isom R , S A B C A D A y C y A
9 isorel F Isom R , S A B D A y A D R y F D S F y
10 5 6 8 9 syl12anc F Isom R , S A B C A D A y C D R y F D S F y
11 10 notbid F Isom R , S A B C A D A y C ¬ D R y ¬ F D S F y
12 11 ralbidva F Isom R , S A B C A D A y C ¬ D R y y C ¬ F D S F y
13 isof1o F Isom R , S A B F : A 1-1 onto B
14 4 13 syl F Isom R , S A B C A D A F : A 1-1 onto B
15 f1ofn F : A 1-1 onto B F Fn A
16 14 15 syl F Isom R , S A B C A D A F Fn A
17 breq2 w = F y F D S w F D S F y
18 17 notbid w = F y ¬ F D S w ¬ F D S F y
19 18 ralima F Fn A C A w F C ¬ F D S w y C ¬ F D S F y
20 16 7 19 syl2anc F Isom R , S A B C A D A w F C ¬ F D S w y C ¬ F D S F y
21 12 20 bitr4d F Isom R , S A B C A D A y C ¬ D R y w F C ¬ F D S w
22 4 adantr F Isom R , S A B C A D A y A F Isom R , S A B
23 simpr F Isom R , S A B C A D A y A y A
24 simplr F Isom R , S A B C A D A y A D A
25 isorel F Isom R , S A B y A D A y R D F y S F D
26 22 23 24 25 syl12anc F Isom R , S A B C A D A y A y R D F y S F D
27 22 adantr F Isom R , S A B C A D A y A z C F Isom R , S A B
28 simplr F Isom R , S A B C A D A y A z C y A
29 7 adantr F Isom R , S A B C A D A y A C A
30 29 sselda F Isom R , S A B C A D A y A z C z A
31 isorel F Isom R , S A B y A z A y R z F y S F z
32 27 28 30 31 syl12anc F Isom R , S A B C A D A y A z C y R z F y S F z
33 32 rexbidva F Isom R , S A B C A D A y A z C y R z z C F y S F z
34 16 adantr F Isom R , S A B C A D A y A F Fn A
35 breq2 v = F z F y S v F y S F z
36 35 rexima F Fn A C A v F C F y S v z C F y S F z
37 34 29 36 syl2anc F Isom R , S A B C A D A y A v F C F y S v z C F y S F z
38 33 37 bitr4d F Isom R , S A B C A D A y A z C y R z v F C F y S v
39 26 38 imbi12d F Isom R , S A B C A D A y A y R D z C y R z F y S F D v F C F y S v
40 39 ralbidva F Isom R , S A B C A D A y A y R D z C y R z y A F y S F D v F C F y S v
41 f1ofo F : A 1-1 onto B F : A onto B
42 breq1 F y = w F y S F D w S F D
43 breq1 F y = w F y S v w S v
44 43 rexbidv F y = w v F C F y S v v F C w S v
45 42 44 imbi12d F y = w F y S F D v F C F y S v w S F D v F C w S v
46 45 cbvfo F : A onto B y A F y S F D v F C F y S v w B w S F D v F C w S v
47 14 41 46 3syl F Isom R , S A B C A D A y A F y S F D v F C F y S v w B w S F D v F C w S v
48 40 47 bitrd F Isom R , S A B C A D A y A y R D z C y R z w B w S F D v F C w S v
49 21 48 anbi12d F Isom R , S A B C A D A y C ¬ D R y y A y R D z C y R z w F C ¬ F D S w w B w S F D v F C w S v
50 3 49 sylan φ D A y C ¬ D R y y A y R D z C y R z w F C ¬ F D S w w B w S F D v F C w S v