Step | Hyp | Ref
| Expression |
1 | | pssnel 4039 |
. . . . . . 7
⊢ (𝑠 ⊊ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) |
2 | 1 | 3ad2ant3 1084 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) → ∃𝑥(𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) |
3 | | mrieqvd.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) |
4 | 3 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) → 𝐴 ∈ (Moore‘𝑋)) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝐴 ∈ (Moore‘𝑋)) |
6 | | mrieqvd.2 |
. . . . . . . 8
⊢ 𝑁 = (mrCls‘𝐴) |
7 | | simprr 796 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → ¬ 𝑥 ∈ 𝑠) |
8 | | difsnb 4337 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝑠 ↔ (𝑠 ∖ {𝑥}) = 𝑠) |
9 | 7, 8 | sylib 208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑠 ∖ {𝑥}) = 𝑠) |
10 | | simpl3 1066 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑠 ⊊ 𝑆) |
11 | 10 | pssssd 3704 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ 𝑆) |
12 | 11 | ssdifd 3746 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑠 ∖ {𝑥}) ⊆ (𝑆 ∖ {𝑥})) |
13 | 9, 12 | eqsstr3d 3640 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ (𝑆 ∖ {𝑥})) |
14 | | mrieqvd.3 |
. . . . . . . . . 10
⊢ 𝐼 = (mrInd‘𝐴) |
15 | | simpl2 1065 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑆 ∈ 𝐼) |
16 | 14, 5, 15 | mrissd 16296 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑆 ⊆ 𝑋) |
17 | 16 | ssdifssd 3748 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑆 ∖ {𝑥}) ⊆ 𝑋) |
18 | 5, 6, 13, 17 | mrcssd 16284 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘𝑠) ⊆ (𝑁‘(𝑆 ∖ {𝑥}))) |
19 | | difssd 3738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑆 ∖ {𝑥}) ⊆ 𝑆) |
20 | 5, 6, 19, 16 | mrcssd 16284 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊆ (𝑁‘𝑆)) |
21 | 5, 6, 16 | mrcssidd 16285 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑆 ⊆ (𝑁‘𝑆)) |
22 | | simprl 794 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑆) |
23 | 21, 22 | sseldd 3604 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → 𝑥 ∈ (𝑁‘𝑆)) |
24 | 6, 14, 5, 15, 22 | ismri2dad 16297 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
25 | 20, 23, 24 | ssnelpssd 3719 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆)) |
26 | 18, 25 | sspsstrd 3715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠)) → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) |
27 | 2, 26 | exlimddv 1863 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) |
28 | 27 | 3expia 1267 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼) → (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) |
29 | 28 | alrimiv 1855 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼) → ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) |
30 | 29 | ex 450 |
. 2
⊢ (𝜑 → (𝑆 ∈ 𝐼 → ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)))) |
31 | 3 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ (Moore‘𝑋)) |
32 | 31 | elfvexd 6222 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑋 ∈ V) |
33 | | mrieqvd.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝑋) |
35 | 32, 34 | ssexd 4805 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑆 ∈ V) |
36 | | difexg 4808 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ V → (𝑆 ∖ {𝑥}) ∈ V) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑆 ∖ {𝑥}) ∈ V) |
38 | | simp1r 1086 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → 𝑥 ∈ 𝑆) |
39 | | difsnpss 4338 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑆 ↔ (𝑆 ∖ {𝑥}) ⊊ 𝑆) |
40 | 38, 39 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑆 ∖ {𝑥}) ⊊ 𝑆) |
41 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → 𝑠 = (𝑆 ∖ {𝑥})) |
42 | 41 | psseq1d 3699 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑠 ⊊ 𝑆 ↔ (𝑆 ∖ {𝑥}) ⊊ 𝑆)) |
43 | 40, 42 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → 𝑠 ⊊ 𝑆) |
44 | | simp3 1063 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) |
45 | 43, 44 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) |
46 | 41 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘𝑠) = (𝑁‘(𝑆 ∖ {𝑥}))) |
47 | 46 | psseq1d 3699 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → ((𝑁‘𝑠) ⊊ (𝑁‘𝑆) ↔ (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆))) |
48 | 45, 47 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆)) |
49 | 48 | 3expia 1267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥})) → ((𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆))) |
50 | 37, 49 | spcimdv 3290 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆))) |
51 | 50 | 3impia 1261 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁‘𝑆)) |
52 | 51 | pssned 3705 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆)) |
53 | 52 | 3com23 1271 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆)) |
54 | 3 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ (Moore‘𝑋)) |
55 | 33 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝑋) |
56 | | simp3 1063 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
57 | 54, 6, 55, 56 | mrieqvlemd 16289 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ (𝑁‘(𝑆 ∖ {𝑥})) = (𝑁‘𝑆))) |
58 | 57 | necon3bbid 2831 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆))) |
59 | 53, 58 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
60 | 59 | 3expia 1267 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → (𝑥 ∈ 𝑆 → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) |
61 | 60 | ralrimiv 2965 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))) → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
62 | 61 | ex 450 |
. . 3
⊢ (𝜑 → (∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) |
63 | 6, 14, 3, 33 | ismri2d 16293 |
. . 3
⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) |
64 | 62, 63 | sylibrd 249 |
. 2
⊢ (𝜑 → (∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)) → 𝑆 ∈ 𝐼)) |
65 | 30, 64 | impbid 202 |
1
⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)))) |