Metamath Proof Explorer


Theorem mreexexlem3d

Description: Base case of the induction in mreexexd . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexexlem2d.1 φ A Moore X
mreexexlem2d.2 N = mrCls A
mreexexlem2d.3 I = mrInd A
mreexexlem2d.4 φ s 𝒫 X y X z N s y N s y N s z
mreexexlem2d.5 φ F X H
mreexexlem2d.6 φ G X H
mreexexlem2d.7 φ F N G H
mreexexlem2d.8 φ F H I
mreexexlem3d.9 φ F = G =
Assertion mreexexlem3d φ i 𝒫 G F i i H I

Proof

Step Hyp Ref Expression
1 mreexexlem2d.1 φ A Moore X
2 mreexexlem2d.2 N = mrCls A
3 mreexexlem2d.3 I = mrInd A
4 mreexexlem2d.4 φ s 𝒫 X y X z N s y N s y N s z
5 mreexexlem2d.5 φ F X H
6 mreexexlem2d.6 φ G X H
7 mreexexlem2d.7 φ F N G H
8 mreexexlem2d.8 φ F H I
9 mreexexlem3d.9 φ F = G =
10 simpr φ F = F =
11 1 adantr φ G = A Moore X
12 7 adantr φ G = F N G H
13 simpr φ G = G =
14 13 uneq1d φ G = G H = H
15 uncom H = H
16 un0 H = H
17 15 16 eqtr3i H = H
18 14 17 eqtrdi φ G = G H = H
19 18 fveq2d φ G = N G H = N H
20 12 19 sseqtrd φ G = F N H
21 8 adantr φ G = F H I
22 3 11 21 mrissd φ G = F H X
23 22 unssbd φ G = H X
24 11 2 23 mrcssidd φ G = H N H
25 20 24 unssd φ G = F H N H
26 ssun2 H F H
27 26 a1i φ G = H F H
28 11 2 3 25 27 21 mrissmrcd φ G = F H = H
29 ssequn1 F H F H = H
30 28 29 sylibr φ G = F H
31 5 adantr φ G = F X H
32 30 31 ssind φ G = F H X H
33 disjdif H X H =
34 32 33 sseqtrdi φ G = F
35 ss0b F F =
36 34 35 sylib φ G = F =
37 10 36 9 mpjaodan φ F =
38 0elpw 𝒫 G
39 37 38 eqeltrdi φ F 𝒫 G
40 1 elfvexd φ X V
41 5 difss2d φ F X
42 40 41 ssexd φ F V
43 enrefg F V F F
44 42 43 syl φ F F
45 breq2 i = F F i F F
46 uneq1 i = F i H = F H
47 46 eleq1d i = F i H I F H I
48 45 47 anbi12d i = F F i i H I F F F H I
49 48 rspcev F 𝒫 G F F F H I i 𝒫 G F i i H I
50 39 44 8 49 syl12anc φ i 𝒫 G F i i H I