| Step | Hyp | Ref
| Expression |
| 1 | | pssnel 4471 |
. . . . . . 7
⊢ (𝑠 ⊊ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) |
| 2 | 1 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) → ∃𝑥(𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) |
| 3 | | mrieqvd.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) |
| 4 | 3 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) → 𝐴 ∈ (Moore‘𝑋)) |
| 5 | 4 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝐴 ∈ (Moore‘𝑋)) |
| 6 | | mrieqvd.2 |
. . . . . . . 8
⊢ 𝑁 = (mrCls‘𝐴) |
| 7 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → ¬ 𝑥 ∈ 𝑠) |
| 8 | | difsnb 4806 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝑠 ↔ (𝑠 ∖ {𝑥}) = 𝑠) |
| 9 | 7, 8 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑠 ∖ {𝑥}) = 𝑠) |
| 10 | | simpl3 1194 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑠 ⊊ 𝑆) |
| 11 | 10 | pssssd 4100 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ 𝑆) |
| 12 | 11 | ssdifd 4145 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑠 ∖ {𝑥}) ⊆ (𝑆 ∖ {𝑥})) |
| 13 | 9, 12 | eqsstrrd 4019 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ (𝑆 ∖ {𝑥})) |
| 14 | | mrieqvd.3 |
. . . . . . . . . 10
⊢ 𝐼 = (mrInd‘𝐴) |
| 15 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑆 ∈ 𝐼) |
| 16 | 14, 5, 15 | mrissd 17679 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑆 ⊆ 𝑋) |
| 17 | 16 | ssdifssd 4147 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑆 ∖ {𝑥}) ⊆ 𝑋) |
| 18 | 5, 6, 13, 17 | mrcssd 17667 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘𝑠) ⊆ (𝑁‘(𝑆 ∖ {𝑥}))) |
| 19 | | difssd 4137 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑆 ∖ {𝑥}) ⊆ 𝑆) |
| 20 | 5, 6, 19, 16 | mrcssd 17667 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊆ (𝑁‘𝑆)) |
| 21 | 5, 6, 16 | mrcssidd 17668 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑆 ⊆ (𝑁‘𝑆)) |
| 22 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑆) |
| 23 | 21, 22 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑥 ∈ (𝑁‘𝑆)) |
| 24 | 6, 14, 5, 15, 22 | ismri2dad 17680 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
| 25 | 20, 23, 24 | ssnelpssd 4115 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆)) |
| 26 | 18, 25 | sspsstrd 4111 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) |
| 27 | 2, 26 | exlimddv 1935 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) |
| 28 | 27 | 3expia 1122 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼) → (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) |
| 29 | 28 | alrimiv 1927 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼) → ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) |
| 30 | 29 | ex 412 |
. 2
⊢ (𝜑 → (𝑆 ∈ 𝐼 → ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)))) |
| 31 | 3 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ (Moore‘𝑋)) |
| 32 | 31 | elfvexd 6945 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑋 ∈ V) |
| 33 | | mrieqvd.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝑋) |
| 35 | 32, 34 | ssexd 5324 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑆 ∈ V) |
| 36 | 35 | difexd 5331 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑆 ∖ {𝑥}) ∈ V) |
| 37 | | simp1r 1199 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → 𝑥 ∈ 𝑆) |
| 38 | | difsnpss 4807 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑆 ↔ (𝑆 ∖ {𝑥}) ⊊ 𝑆) |
| 39 | 37, 38 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑆 ∖ {𝑥}) ⊊ 𝑆) |
| 40 | | simp2 1138 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → 𝑠 = (𝑆 ∖ {𝑥})) |
| 41 | 40 | psseq1d 4095 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑠 ⊊ 𝑆 ↔ (𝑆 ∖ {𝑥}) ⊊ 𝑆)) |
| 42 | 39, 41 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → 𝑠 ⊊ 𝑆) |
| 43 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) |
| 44 | 42, 43 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) |
| 45 | 40 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘𝑠) = (𝑁‘(𝑆 ∖ {𝑥}))) |
| 46 | 45 | psseq1d 4095 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → ((𝑁‘𝑠) ⊊ (𝑁‘𝑆) ↔ (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆))) |
| 47 | 44, 46 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆)) |
| 48 | 47 | 3expia 1122 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥})) → ((𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆))) |
| 49 | 36, 48 | spcimdv 3593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆))) |
| 50 | 49 | 3impia 1118 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆)) |
| 51 | 50 | pssned 4101 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆)) |
| 52 | 51 | 3com23 1127 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆)) |
| 53 | 3 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ (Moore‘𝑋)) |
| 54 | 33 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝑋) |
| 55 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
| 56 | 53, 6, 54, 55 | mrieqvlemd 17672 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ (𝑁‘(𝑆 ∖ {𝑥})) = (𝑁‘𝑆))) |
| 57 | 56 | necon3bbid 2978 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆))) |
| 58 | 52, 57 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
| 59 | 58 | 3expia 1122 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑥 ∈ 𝑆 → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) |
| 60 | 59 | ralrimiv 3145 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
| 61 | 60 | ex 412 |
. . 3
⊢ (𝜑 → (∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) |
| 62 | 6, 14, 3, 33 | ismri2d 17676 |
. . 3
⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) |
| 63 | 61, 62 | sylibrd 259 |
. 2
⊢ (𝜑 → (∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → 𝑆 ∈ 𝐼)) |
| 64 | 30, 63 | impbid 212 |
1
⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)))) |