| Step | Hyp | Ref
| Expression |
| 1 | | mreexmrid.2 |
. 2
⊢ 𝑁 = (mrCls‘𝐴) |
| 2 | | mreexmrid.3 |
. 2
⊢ 𝐼 = (mrInd‘𝐴) |
| 3 | | mreexmrid.1 |
. 2
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) |
| 4 | | mreexmrid.5 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝐼) |
| 5 | 2, 3, 4 | mrissd 17679 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
| 6 | | mreexmrid.6 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑋) |
| 7 | 6 | snssd 4809 |
. . 3
⊢ (𝜑 → {𝑌} ⊆ 𝑋) |
| 8 | 5, 7 | unssd 4192 |
. 2
⊢ (𝜑 → (𝑆 ∪ {𝑌}) ⊆ 𝑋) |
| 9 | 3 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → 𝐴 ∈ (Moore‘𝑋)) |
| 10 | 9 | elfvexd 6945 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → 𝑋 ∈ V) |
| 11 | | mreexmrid.4 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) |
| 12 | 11 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) |
| 13 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → 𝑆 ∈ 𝐼) |
| 14 | 2, 9, 13 | mrissd 17679 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → 𝑆 ⊆ 𝑋) |
| 15 | 14 | ssdifssd 4147 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → (𝑆 ∖ {𝑥}) ⊆ 𝑋) |
| 16 | 6 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → 𝑌 ∈ 𝑋) |
| 17 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) |
| 18 | | difundir 4291 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∪ {𝑌}) ∖ {𝑥}) = ((𝑆 ∖ {𝑥}) ∪ ({𝑌} ∖ {𝑥})) |
| 19 | | simp2 1138 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → 𝑥 ∈ 𝑆) |
| 20 | 3, 1, 5 | mrcssidd 17668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑆)) |
| 21 | | mreexmrid.7 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘𝑆)) |
| 22 | 20, 21 | ssneldd 3986 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ 𝑌 ∈ 𝑆) |
| 23 | 22 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ¬ 𝑌 ∈ 𝑆) |
| 24 | | nelneq 2865 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑆 ∧ ¬ 𝑌 ∈ 𝑆) → ¬ 𝑥 = 𝑌) |
| 25 | 19, 23, 24 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ¬ 𝑥 = 𝑌) |
| 26 | | elsni 4643 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {𝑌} → 𝑥 = 𝑌) |
| 27 | 25, 26 | nsyl 140 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ¬ 𝑥 ∈ {𝑌}) |
| 28 | | difsnb 4806 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑥 ∈ {𝑌} ↔ ({𝑌} ∖ {𝑥}) = {𝑌}) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ({𝑌} ∖ {𝑥}) = {𝑌}) |
| 30 | 29 | uneq2d 4168 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ((𝑆 ∖ {𝑥}) ∪ ({𝑌} ∖ {𝑥})) = ((𝑆 ∖ {𝑥}) ∪ {𝑌})) |
| 31 | 18, 30 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ((𝑆 ∪ {𝑌}) ∖ {𝑥}) = ((𝑆 ∖ {𝑥}) ∪ {𝑌})) |
| 32 | 31 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥})) = (𝑁‘((𝑆 ∖ {𝑥}) ∪ {𝑌}))) |
| 33 | 17, 32 | eleqtrd 2843 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → 𝑥 ∈ (𝑁‘((𝑆 ∖ {𝑥}) ∪ {𝑌}))) |
| 34 | 1, 2, 9, 13, 19 | ismri2dad 17680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
| 35 | 10, 12, 15, 16, 33, 34 | mreexd 17685 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → 𝑌 ∈ (𝑁‘((𝑆 ∖ {𝑥}) ∪ {𝑥}))) |
| 36 | 21 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ¬ 𝑌 ∈ (𝑁‘𝑆)) |
| 37 | | undif1 4476 |
. . . . . . . . . . 11
⊢ ((𝑆 ∖ {𝑥}) ∪ {𝑥}) = (𝑆 ∪ {𝑥}) |
| 38 | 19 | snssd 4809 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → {𝑥} ⊆ 𝑆) |
| 39 | | ssequn2 4189 |
. . . . . . . . . . . 12
⊢ ({𝑥} ⊆ 𝑆 ↔ (𝑆 ∪ {𝑥}) = 𝑆) |
| 40 | 38, 39 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → (𝑆 ∪ {𝑥}) = 𝑆) |
| 41 | 37, 40 | eqtrid 2789 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ((𝑆 ∖ {𝑥}) ∪ {𝑥}) = 𝑆) |
| 42 | 41 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → (𝑁‘((𝑆 ∖ {𝑥}) ∪ {𝑥})) = (𝑁‘𝑆)) |
| 43 | 36, 42 | neleqtrrd 2864 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) → ¬ 𝑌 ∈ (𝑁‘((𝑆 ∖ {𝑥}) ∪ {𝑥}))) |
| 44 | 35, 43 | pm2.65i 194 |
. . . . . . 7
⊢ ¬
(𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) |
| 45 | | df-3an 1089 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) ↔ ((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥})))) |
| 46 | 44, 45 | mtbi 322 |
. . . . . 6
⊢ ¬
((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) |
| 47 | 46 | imnani 400 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) |
| 48 | 47 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) |
| 49 | 26 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → 𝑥 = 𝑌) |
| 50 | 21 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → ¬ 𝑌 ∈ (𝑁‘𝑆)) |
| 51 | 49, 50 | eqneltrd 2861 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → ¬ 𝑥 ∈ (𝑁‘𝑆)) |
| 52 | 49 | sneqd 4638 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → {𝑥} = {𝑌}) |
| 53 | 52 | difeq2d 4126 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → ((𝑆 ∪ {𝑌}) ∖ {𝑥}) = ((𝑆 ∪ {𝑌}) ∖ {𝑌})) |
| 54 | | difun2 4481 |
. . . . . . . 8
⊢ ((𝑆 ∪ {𝑌}) ∖ {𝑌}) = (𝑆 ∖ {𝑌}) |
| 55 | 53, 54 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → ((𝑆 ∪ {𝑌}) ∖ {𝑥}) = (𝑆 ∖ {𝑌})) |
| 56 | | difsnb 4806 |
. . . . . . . . 9
⊢ (¬
𝑌 ∈ 𝑆 ↔ (𝑆 ∖ {𝑌}) = 𝑆) |
| 57 | 22, 56 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 ∖ {𝑌}) = 𝑆) |
| 58 | 57 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → (𝑆 ∖ {𝑌}) = 𝑆) |
| 59 | 55, 58 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → ((𝑆 ∪ {𝑌}) ∖ {𝑥}) = 𝑆) |
| 60 | 59 | fveq2d 6910 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥})) = (𝑁‘𝑆)) |
| 61 | 51, 60 | neleqtrrd 2864 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) ∧ 𝑥 ∈ {𝑌}) → ¬ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) |
| 62 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) → 𝑥 ∈ (𝑆 ∪ {𝑌})) |
| 63 | | elun 4153 |
. . . . 5
⊢ (𝑥 ∈ (𝑆 ∪ {𝑌}) ↔ (𝑥 ∈ 𝑆 ∨ 𝑥 ∈ {𝑌})) |
| 64 | 62, 63 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) → (𝑥 ∈ 𝑆 ∨ 𝑥 ∈ {𝑌})) |
| 65 | 48, 61, 64 | mpjaodan 961 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∪ {𝑌})) → ¬ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) |
| 66 | 65 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (𝑆 ∪ {𝑌}) ¬ 𝑥 ∈ (𝑁‘((𝑆 ∪ {𝑌}) ∖ {𝑥}))) |
| 67 | 1, 2, 3, 8, 66 | ismri2dd 17677 |
1
⊢ (𝜑 → (𝑆 ∪ {𝑌}) ∈ 𝐼) |