Metamath Proof Explorer


Theorem icccmplem1

Description: Lemma for icccmp . (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses icccmp.1 J = topGen ran .
icccmp.2 T = J 𝑡 A B
icccmp.3 D = abs 2
icccmp.4 S = x A B | z 𝒫 U Fin A x z
icccmp.5 φ A
icccmp.6 φ B
icccmp.7 φ A B
icccmp.8 φ U J
icccmp.9 φ A B U
Assertion icccmplem1 φ A S y S y B

Proof

Step Hyp Ref Expression
1 icccmp.1 J = topGen ran .
2 icccmp.2 T = J 𝑡 A B
3 icccmp.3 D = abs 2
4 icccmp.4 S = x A B | z 𝒫 U Fin A x z
5 icccmp.5 φ A
6 icccmp.6 φ B
7 icccmp.7 φ A B
8 icccmp.8 φ U J
9 icccmp.9 φ A B U
10 5 rexrd φ A *
11 6 rexrd φ B *
12 lbicc2 A * B * A B A A B
13 10 11 7 12 syl3anc φ A A B
14 9 13 sseldd φ A U
15 eluni2 A U u U A u
16 14 15 sylib φ u U A u
17 snssi u U u U
18 17 ad2antrl φ u U A u u U
19 snex u V
20 19 elpw u 𝒫 U u U
21 18 20 sylibr φ u U A u u 𝒫 U
22 snfi u Fin
23 22 a1i φ u U A u u Fin
24 21 23 elind φ u U A u u 𝒫 U Fin
25 10 adantr φ u U A u A *
26 iccid A * A A = A
27 25 26 syl φ u U A u A A = A
28 snssi A u A u
29 28 ad2antll φ u U A u A u
30 27 29 eqsstrd φ u U A u A A u
31 unieq z = u z = u
32 vex u V
33 32 unisn u = u
34 31 33 eqtrdi z = u z = u
35 34 sseq2d z = u A A z A A u
36 35 rspcev u 𝒫 U Fin A A u z 𝒫 U Fin A A z
37 24 30 36 syl2anc φ u U A u z 𝒫 U Fin A A z
38 16 37 rexlimddv φ z 𝒫 U Fin A A z
39 oveq2 x = A A x = A A
40 39 sseq1d x = A A x z A A z
41 40 rexbidv x = A z 𝒫 U Fin A x z z 𝒫 U Fin A A z
42 41 4 elrab2 A S A A B z 𝒫 U Fin A A z
43 13 38 42 sylanbrc φ A S
44 4 ssrab3 S A B
45 44 sseli y S y A B
46 elicc2 A B y A B y A y y B
47 5 6 46 syl2anc φ y A B y A y y B
48 47 biimpa φ y A B y A y y B
49 48 simp3d φ y A B y B
50 45 49 sylan2 φ y S y B
51 50 ralrimiva φ y S y B
52 43 51 jca φ A S y S y B