Metamath Proof Explorer


Theorem isf34lem4

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a F = x 𝒫 A A x
Assertion isf34lem4 A V X 𝒫 A X F X = F X

Proof

Step Hyp Ref Expression
1 compss.a F = x 𝒫 A A x
2 sspwuni X 𝒫 A X A
3 1 isf34lem1 A V X A F X = A X
4 2 3 sylan2b A V X 𝒫 A F X = A X
5 4 adantrr A V X 𝒫 A X F X = A X
6 simplrr A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X ¬ b X
7 simprl A V X 𝒫 A X b A ¬ b X b A
8 7 ad2antrr A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X ¬ b a b A
9 simpr A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X ¬ b a ¬ b a
10 8 9 eldifd A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X ¬ b a b A a
11 simplrr A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X ¬ b a A a X
12 elunii b A a A a X b X
13 10 11 12 syl2anc A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X ¬ b a b X
14 13 ex A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X ¬ b a b X
15 6 14 mt3d A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X b a
16 15 expr A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X b a
17 16 ralrimiva A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X b a
18 17 ex A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X b a
19 n0 X c c X
20 simpr A V X 𝒫 A X 𝒫 A
21 20 sselda A V X 𝒫 A c X c 𝒫 A
22 21 elpwid A V X 𝒫 A c X c A
23 dfss4 c A A A c = c
24 22 23 sylib A V X 𝒫 A c X A A c = c
25 simpr A V X 𝒫 A c X c X
26 24 25 eqeltrd A V X 𝒫 A c X A A c X
27 difss A c A
28 elpw2g A V A c 𝒫 A A c A
29 27 28 mpbiri A V A c 𝒫 A
30 29 ad2antrr A V X 𝒫 A c X A c 𝒫 A
31 difeq2 a = A c A a = A A c
32 31 eleq1d a = A c A a X A A c X
33 eleq2 a = A c b a b A c
34 32 33 imbi12d a = A c A a X b a A A c X b A c
35 34 rspcv A c 𝒫 A a 𝒫 A A a X b a A A c X b A c
36 30 35 syl A V X 𝒫 A c X a 𝒫 A A a X b a A A c X b A c
37 26 36 mpid A V X 𝒫 A c X a 𝒫 A A a X b a b A c
38 eldifi b A c b A
39 37 38 syl6 A V X 𝒫 A c X a 𝒫 A A a X b a b A
40 39 ex A V X 𝒫 A c X a 𝒫 A A a X b a b A
41 40 exlimdv A V X 𝒫 A c c X a 𝒫 A A a X b a b A
42 19 41 syl5bi A V X 𝒫 A X a 𝒫 A A a X b a b A
43 42 impr A V X 𝒫 A X a 𝒫 A A a X b a b A
44 eluni b X c b c c X
45 29 ad2antrr A V X 𝒫 A X b c c X A c 𝒫 A
46 26 adantlrr A V X 𝒫 A X c X A A c X
47 46 adantrl A V X 𝒫 A X b c c X A A c X
48 elndif b c ¬ b A c
49 48 ad2antrl A V X 𝒫 A X b c c X ¬ b A c
50 47 49 jcn A V X 𝒫 A X b c c X ¬ A A c X b A c
51 34 notbid a = A c ¬ A a X b a ¬ A A c X b A c
52 51 rspcev A c 𝒫 A ¬ A A c X b A c a 𝒫 A ¬ A a X b a
53 45 50 52 syl2anc A V X 𝒫 A X b c c X a 𝒫 A ¬ A a X b a
54 rexnal a 𝒫 A ¬ A a X b a ¬ a 𝒫 A A a X b a
55 53 54 sylib A V X 𝒫 A X b c c X ¬ a 𝒫 A A a X b a
56 55 ex A V X 𝒫 A X b c c X ¬ a 𝒫 A A a X b a
57 56 exlimdv A V X 𝒫 A X c b c c X ¬ a 𝒫 A A a X b a
58 44 57 syl5bi A V X 𝒫 A X b X ¬ a 𝒫 A A a X b a
59 58 con2d A V X 𝒫 A X a 𝒫 A A a X b a ¬ b X
60 43 59 jcad A V X 𝒫 A X a 𝒫 A A a X b a b A ¬ b X
61 18 60 impbid A V X 𝒫 A X b A ¬ b X a 𝒫 A A a X b a
62 eldif b A X b A ¬ b X
63 vex b V
64 63 elintrab b a 𝒫 A | A a X a 𝒫 A A a X b a
65 61 62 64 3bitr4g A V X 𝒫 A X b A X b a 𝒫 A | A a X
66 65 eqrdv A V X 𝒫 A X A X = a 𝒫 A | A a X
67 5 66 eqtrd A V X 𝒫 A X F X = a 𝒫 A | A a X
68 1 compss F X = a 𝒫 A | A a X
69 68 inteqi F X = a 𝒫 A | A a X
70 67 69 syl6eqr A V X 𝒫 A X F X = F X