Step | Hyp | Ref
| Expression |
1 | | pssnel 4360 |
. . . . . . 7
⊢ (𝑠 ⊊ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) |
2 | 1 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) → ∃𝑥(𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) |
3 | | mrieqvd.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) |
4 | 3 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) → 𝐴 ∈ (Moore‘𝑋)) |
5 | 4 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝐴 ∈ (Moore‘𝑋)) |
6 | | mrieqvd.2 |
. . . . . . . 8
⊢ 𝑁 = (mrCls‘𝐴) |
7 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → ¬ 𝑥 ∈ 𝑠) |
8 | | difsnb 4694 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝑠 ↔ (𝑠 ∖ {𝑥}) = 𝑠) |
9 | 7, 8 | sylib 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑠 ∖ {𝑥}) = 𝑠) |
10 | | simpl3 1194 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑠 ⊊ 𝑆) |
11 | 10 | pssssd 3988 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ 𝑆) |
12 | 11 | ssdifd 4031 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑠 ∖ {𝑥}) ⊆ (𝑆 ∖ {𝑥})) |
13 | 9, 12 | eqsstrrd 3916 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ (𝑆 ∖ {𝑥})) |
14 | | mrieqvd.3 |
. . . . . . . . . 10
⊢ 𝐼 = (mrInd‘𝐴) |
15 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑆 ∈ 𝐼) |
16 | 14, 5, 15 | mrissd 17010 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑆 ⊆ 𝑋) |
17 | 16 | ssdifssd 4033 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑆 ∖ {𝑥}) ⊆ 𝑋) |
18 | 5, 6, 13, 17 | mrcssd 16998 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘𝑠) ⊆ (𝑁‘(𝑆 ∖ {𝑥}))) |
19 | | difssd 4023 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑆 ∖ {𝑥}) ⊆ 𝑆) |
20 | 5, 6, 19, 16 | mrcssd 16998 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊆ (𝑁‘𝑆)) |
21 | 5, 6, 16 | mrcssidd 16999 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑆 ⊆ (𝑁‘𝑆)) |
22 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑆) |
23 | 21, 22 | sseldd 3878 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑥 ∈ (𝑁‘𝑆)) |
24 | 6, 14, 5, 15, 22 | ismri2dad 17011 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
25 | 20, 23, 24 | ssnelpssd 4003 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆)) |
26 | 18, 25 | sspsstrd 3999 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) |
27 | 2, 26 | exlimddv 1942 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) |
28 | 27 | 3expia 1122 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼) → (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) |
29 | 28 | alrimiv 1934 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼) → ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) |
30 | 29 | ex 416 |
. 2
⊢ (𝜑 → (𝑆 ∈ 𝐼 → ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)))) |
31 | 3 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ (Moore‘𝑋)) |
32 | 31 | elfvexd 6708 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑋 ∈ V) |
33 | | mrieqvd.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
34 | 33 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝑋) |
35 | 32, 34 | ssexd 5192 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑆 ∈ V) |
36 | 35 | difexd 5197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑆 ∖ {𝑥}) ∈ V) |
37 | | simp1r 1199 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → 𝑥 ∈ 𝑆) |
38 | | difsnpss 4695 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑆 ↔ (𝑆 ∖ {𝑥}) ⊊ 𝑆) |
39 | 37, 38 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑆 ∖ {𝑥}) ⊊ 𝑆) |
40 | | simp2 1138 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → 𝑠 = (𝑆 ∖ {𝑥})) |
41 | 40 | psseq1d 3983 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑠 ⊊ 𝑆 ↔ (𝑆 ∖ {𝑥}) ⊊ 𝑆)) |
42 | 39, 41 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → 𝑠 ⊊ 𝑆) |
43 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) |
44 | 42, 43 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) |
45 | 40 | fveq2d 6678 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘𝑠) = (𝑁‘(𝑆 ∖ {𝑥}))) |
46 | 45 | psseq1d 3983 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → ((𝑁‘𝑠) ⊊ (𝑁‘𝑆) ↔ (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆))) |
47 | 44, 46 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆)) |
48 | 47 | 3expia 1122 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥})) → ((𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆))) |
49 | 36, 48 | spcimdv 3497 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆))) |
50 | 49 | 3impia 1118 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆)) |
51 | 50 | pssned 3989 |
. . . . . . . 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 17003 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ (𝑁‘(𝑆 ∖ {𝑥})) = (𝑁‘𝑆))) |
57 | 56 | necon3bbid 2971 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆))) |
58 | 52, 57 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
59 | 58 | 3expia 1122 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑥 ∈ 𝑆 → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) |
60 | 59 | ralrimiv 3095 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
61 | 60 | ex 416 |
. . 3
⊢ (𝜑 → (∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) |
62 | 6, 14, 3, 33 | ismri2d 17007 |
. . 3
⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) |
63 | 61, 62 | sylibrd 262 |
. 2
⊢ (𝜑 → (∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → 𝑆 ∈ 𝐼)) |
64 | 30, 63 | impbid 215 |
1
⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)))) |