Proof of Theorem mreexexlem2d
| Step | Hyp | Ref
| Expression |
| 1 | | mreexexlem2d.7 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) |
| 2 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) |
| 3 | | mreexexlem2d.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) |
| 4 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐴 ∈ (Moore‘𝑋)) |
| 5 | | mreexexlem2d.2 |
. . . . . . . . 9
⊢ 𝑁 = (mrCls‘𝐴) |
| 6 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 7 | | ssun2 4179 |
. . . . . . . . . . . . 13
⊢ 𝐻 ⊆ ((𝐹 ∖ {𝑌}) ∪ 𝐻) |
| 8 | | difundir 4291 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∪ 𝐻) ∖ {𝑌}) = ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∖ {𝑌})) |
| 9 | | mreexexlem2d.9 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑌 ∈ 𝐹) |
| 10 | | incom 4209 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∩ 𝐻) = (𝐻 ∩ 𝐹) |
| 11 | | mreexexlem2d.5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) |
| 12 | | ssdifin0 4486 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ⊆ (𝑋 ∖ 𝐻) → (𝐹 ∩ 𝐻) = ∅) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹 ∩ 𝐻) = ∅) |
| 14 | 10, 13 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐻 ∩ 𝐹) = ∅) |
| 15 | | minel 4466 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑌 ∈ 𝐹 ∧ (𝐻 ∩ 𝐹) = ∅) → ¬ 𝑌 ∈ 𝐻) |
| 16 | 9, 14, 15 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ 𝑌 ∈ 𝐻) |
| 17 | | difsnb 4806 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑌 ∈ 𝐻 ↔ (𝐻 ∖ {𝑌}) = 𝐻) |
| 18 | 16, 17 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐻 ∖ {𝑌}) = 𝐻) |
| 19 | 18 | uneq2d 4168 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∖ {𝑌})) = ((𝐹 ∖ {𝑌}) ∪ 𝐻)) |
| 20 | 8, 19 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∪ 𝐻) ∖ {𝑌}) = ((𝐹 ∖ {𝑌}) ∪ 𝐻)) |
| 21 | 7, 20 | sseqtrrid 4027 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ⊆ ((𝐹 ∪ 𝐻) ∖ {𝑌})) |
| 22 | | mreexexlem2d.3 |
. . . . . . . . . . . . . . 15
⊢ 𝐼 = (mrInd‘𝐴) |
| 23 | | mreexexlem2d.8 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) |
| 24 | 22, 3, 23 | mrissd 17679 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∪ 𝐻) ⊆ 𝑋) |
| 25 | 24 | ssdifssd 4147 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∪ 𝐻) ∖ {𝑌}) ⊆ 𝑋) |
| 26 | 3, 5, 25 | mrcssidd 17668 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ∪ 𝐻) ∖ {𝑌}) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 27 | 21, 26 | sstrd 3994 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 28 | 27 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐻 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 29 | 6, 28 | unssd 4192 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝐺 ∪ 𝐻) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 30 | 4, 5 | mrcssvd 17666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})) ⊆ 𝑋) |
| 31 | 4, 5, 29, 30 | mrcssd 17667 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑁‘(𝐺 ∪ 𝐻)) ⊆ (𝑁‘(𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) |
| 32 | 25 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → ((𝐹 ∪ 𝐻) ∖ {𝑌}) ⊆ 𝑋) |
| 33 | 4, 5, 32 | mrcidmd 17669 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑁‘(𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) = (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 34 | 31, 33 | sseqtrd 4020 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑁‘(𝐺 ∪ 𝐻)) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 35 | 2, 34 | sstrd 3994 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐹 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 36 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝑌 ∈ 𝐹) |
| 37 | 35, 36 | sseldd 3984 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝑌 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 38 | 23 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝐹 ∪ 𝐻) ∈ 𝐼) |
| 39 | | ssun1 4178 |
. . . . . . 7
⊢ 𝐹 ⊆ (𝐹 ∪ 𝐻) |
| 40 | 39, 36 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝑌 ∈ (𝐹 ∪ 𝐻)) |
| 41 | 5, 22, 4, 38, 40 | ismri2dad 17680 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → ¬ 𝑌 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 42 | 37, 41 | pm2.65da 817 |
. . . 4
⊢ (𝜑 → ¬ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 43 | | nss 4048 |
. . . 4
⊢ (¬
𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})) ↔ ∃𝑔(𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) |
| 44 | 42, 43 | sylib 218 |
. . 3
⊢ (𝜑 → ∃𝑔(𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) |
| 45 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝑔 ∈ 𝐺) |
| 46 | | ssun1 4178 |
. . . . . . . . . 10
⊢ (𝐹 ∖ {𝑌}) ⊆ ((𝐹 ∖ {𝑌}) ∪ 𝐻) |
| 47 | 46, 20 | sseqtrrid 4027 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∖ {𝑌}) ⊆ ((𝐹 ∪ 𝐻) ∖ {𝑌})) |
| 48 | 47, 26 | sstrd 3994 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∖ {𝑌}) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (𝐹 ∖ {𝑌}) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 50 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) |
| 51 | 49, 50 | ssneldd 3986 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ¬ 𝑔 ∈ (𝐹 ∖ {𝑌})) |
| 52 | | unass 4172 |
. . . . . . 7
⊢ (((𝐹 ∖ {𝑌}) ∪ 𝐻) ∪ {𝑔}) = ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) |
| 53 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝐴 ∈ (Moore‘𝑋)) |
| 54 | | mreexexlem2d.4 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) |
| 55 | 54 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) |
| 56 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (𝐹 ∪ 𝐻) ∈ 𝐼) |
| 57 | | difss 4136 |
. . . . . . . . . 10
⊢ (𝐹 ∖ {𝑌}) ⊆ 𝐹 |
| 58 | | unss1 4185 |
. . . . . . . . . 10
⊢ ((𝐹 ∖ {𝑌}) ⊆ 𝐹 → ((𝐹 ∖ {𝑌}) ∪ 𝐻) ⊆ (𝐹 ∪ 𝐻)) |
| 59 | 57, 58 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ((𝐹 ∖ {𝑌}) ∪ 𝐻) ⊆ (𝐹 ∪ 𝐻)) |
| 60 | 53, 5, 22, 56, 59 | mrissmrid 17684 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ((𝐹 ∖ {𝑌}) ∪ 𝐻) ∈ 𝐼) |
| 61 | | mreexexlem2d.6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) |
| 62 | 61 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝐺 ⊆ (𝑋 ∖ 𝐻)) |
| 63 | 62 | difss2d 4139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝐺 ⊆ 𝑋) |
| 64 | 63, 45 | sseldd 3984 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝑔 ∈ 𝑋) |
| 65 | 20 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ((𝐹 ∪ 𝐻) ∖ {𝑌}) = ((𝐹 ∖ {𝑌}) ∪ 𝐻)) |
| 66 | 65 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})) = (𝑁‘((𝐹 ∖ {𝑌}) ∪ 𝐻))) |
| 67 | 50, 66 | neleqtrd 2863 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ¬ 𝑔 ∈ (𝑁‘((𝐹 ∖ {𝑌}) ∪ 𝐻))) |
| 68 | 53, 5, 22, 55, 60, 64, 67 | mreexmrid 17686 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (((𝐹 ∖ {𝑌}) ∪ 𝐻) ∪ {𝑔}) ∈ 𝐼) |
| 69 | 52, 68 | eqeltrrid 2846 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼) |
| 70 | 45, 51, 69 | jca32 515 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼))) |
| 71 | 70 | ex 412 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼)))) |
| 72 | 71 | eximdv 1917 |
. . 3
⊢ (𝜑 → (∃𝑔(𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → ∃𝑔(𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼)))) |
| 73 | 44, 72 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑔(𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼))) |
| 74 | | df-rex 3071 |
. 2
⊢
(∃𝑔 ∈
𝐺 (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼) ↔ ∃𝑔(𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼))) |
| 75 | 73, 74 | sylibr 234 |
1
⊢ (𝜑 → ∃𝑔 ∈ 𝐺 (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼)) |