Metamath Proof Explorer


Theorem mreexexlem2d

Description: Used in mreexexlem4d to prove the induction step in mreexexd . See the proof of Proposition 4.2.1 in FaureFrolicher p. 86 to 87. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexexlem2d.1 ( 𝜑𝐴 ∈ ( Moore ‘ 𝑋 ) )
mreexexlem2d.2 𝑁 = ( mrCls ‘ 𝐴 )
mreexexlem2d.3 𝐼 = ( mrInd ‘ 𝐴 )
mreexexlem2d.4 ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
mreexexlem2d.5 ( 𝜑𝐹 ⊆ ( 𝑋𝐻 ) )
mreexexlem2d.6 ( 𝜑𝐺 ⊆ ( 𝑋𝐻 ) )
mreexexlem2d.7 ( 𝜑𝐹 ⊆ ( 𝑁 ‘ ( 𝐺𝐻 ) ) )
mreexexlem2d.8 ( 𝜑 → ( 𝐹𝐻 ) ∈ 𝐼 )
mreexexlem2d.9 ( 𝜑𝑌𝐹 )
Assertion mreexexlem2d ( 𝜑 → ∃ 𝑔𝐺 ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 mreexexlem2d.1 ( 𝜑𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mreexexlem2d.2 𝑁 = ( mrCls ‘ 𝐴 )
3 mreexexlem2d.3 𝐼 = ( mrInd ‘ 𝐴 )
4 mreexexlem2d.4 ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
5 mreexexlem2d.5 ( 𝜑𝐹 ⊆ ( 𝑋𝐻 ) )
6 mreexexlem2d.6 ( 𝜑𝐺 ⊆ ( 𝑋𝐻 ) )
7 mreexexlem2d.7 ( 𝜑𝐹 ⊆ ( 𝑁 ‘ ( 𝐺𝐻 ) ) )
8 mreexexlem2d.8 ( 𝜑 → ( 𝐹𝐻 ) ∈ 𝐼 )
9 mreexexlem2d.9 ( 𝜑𝑌𝐹 )
10 7 adantr ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺𝐻 ) ) )
11 1 adantr ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
12 simpr ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
13 ssun2 𝐻 ⊆ ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 )
14 difundir ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∖ { 𝑌 } ) )
15 incom ( 𝐹𝐻 ) = ( 𝐻𝐹 )
16 ssdifin0 ( 𝐹 ⊆ ( 𝑋𝐻 ) → ( 𝐹𝐻 ) = ∅ )
17 5 16 syl ( 𝜑 → ( 𝐹𝐻 ) = ∅ )
18 15 17 eqtr3id ( 𝜑 → ( 𝐻𝐹 ) = ∅ )
19 minel ( ( 𝑌𝐹 ∧ ( 𝐻𝐹 ) = ∅ ) → ¬ 𝑌𝐻 )
20 9 18 19 syl2anc ( 𝜑 → ¬ 𝑌𝐻 )
21 difsnb ( ¬ 𝑌𝐻 ↔ ( 𝐻 ∖ { 𝑌 } ) = 𝐻 )
22 20 21 sylib ( 𝜑 → ( 𝐻 ∖ { 𝑌 } ) = 𝐻 )
23 22 uneq2d ( 𝜑 → ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∖ { 𝑌 } ) ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) )
24 14 23 eqtrid ( 𝜑 → ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) )
25 13 24 sseqtrrid ( 𝜑𝐻 ⊆ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) )
26 3 1 8 mrissd ( 𝜑 → ( 𝐹𝐻 ) ⊆ 𝑋 )
27 26 ssdifssd ( 𝜑 → ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ⊆ 𝑋 )
28 1 2 27 mrcssidd ( 𝜑 → ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
29 25 28 sstrd ( 𝜑𝐻 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
30 29 adantr ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐻 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
31 12 30 unssd ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝐺𝐻 ) ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
32 11 2 mrcssvd ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ⊆ 𝑋 )
33 11 2 31 32 mrcssd ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ ( 𝐺𝐻 ) ) ⊆ ( 𝑁 ‘ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) )
34 27 adantr ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ⊆ 𝑋 )
35 11 2 34 mrcidmd ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) = ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
36 33 35 sseqtrd ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ ( 𝐺𝐻 ) ) ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
37 10 36 sstrd ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐹 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
38 9 adantr ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → 𝑌𝐹 )
39 37 38 sseldd ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
40 8 adantr ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝐹𝐻 ) ∈ 𝐼 )
41 ssun1 𝐹 ⊆ ( 𝐹𝐻 )
42 41 38 sselid ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → 𝑌 ∈ ( 𝐹𝐻 ) )
43 2 3 11 40 42 ismri2dad ( ( 𝜑𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ¬ 𝑌 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
44 39 43 pm2.65da ( 𝜑 → ¬ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
45 nss ( ¬ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ↔ ∃ 𝑔 ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) )
46 44 45 sylib ( 𝜑 → ∃ 𝑔 ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) )
47 simprl ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝑔𝐺 )
48 ssun1 ( 𝐹 ∖ { 𝑌 } ) ⊆ ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 )
49 48 24 sseqtrrid ( 𝜑 → ( 𝐹 ∖ { 𝑌 } ) ⊆ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) )
50 49 28 sstrd ( 𝜑 → ( 𝐹 ∖ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
51 50 adantr ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( 𝐹 ∖ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
52 simprr ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) )
53 51 52 ssneldd ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) )
54 unass ( ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ∪ { 𝑔 } ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) )
55 1 adantr ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
56 4 adantr ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ∀ 𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
57 8 adantr ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( 𝐹𝐻 ) ∈ 𝐼 )
58 difss ( 𝐹 ∖ { 𝑌 } ) ⊆ 𝐹
59 unss1 ( ( 𝐹 ∖ { 𝑌 } ) ⊆ 𝐹 → ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ⊆ ( 𝐹𝐻 ) )
60 58 59 mp1i ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ⊆ ( 𝐹𝐻 ) )
61 55 2 3 57 60 mrissmrid ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ∈ 𝐼 )
62 6 adantr ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝐺 ⊆ ( 𝑋𝐻 ) )
63 62 difss2d ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝐺𝑋 )
64 63 47 sseldd ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝑔𝑋 )
65 24 adantr ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) )
66 65 fveq2d ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ) )
67 52 66 neleqtrd ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ) )
68 55 2 3 56 61 64 67 mreexmrid ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ∪ { 𝑔 } ) ∈ 𝐼 )
69 54 68 eqeltrrid ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 )
70 47 53 69 jca32 ( ( 𝜑 ∧ ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( 𝑔𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) )
71 70 ex ( 𝜑 → ( ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑔𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) ) )
72 71 eximdv ( 𝜑 → ( ∃ 𝑔 ( 𝑔𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹𝐻 ) ∖ { 𝑌 } ) ) ) → ∃ 𝑔 ( 𝑔𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) ) )
73 46 72 mpd ( 𝜑 → ∃ 𝑔 ( 𝑔𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) )
74 df-rex ( ∃ 𝑔𝐺 ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ↔ ∃ 𝑔 ( 𝑔𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) )
75 73 74 sylibr ( 𝜑 → ∃ 𝑔𝐺 ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) )