Step | Hyp | Ref
| Expression |
1 | | bren 6681 |
. . . . . . 7
⊢ (𝐴 ≈ 𝐵 ↔ ∃ℎ ℎ:𝐴–1-1-onto→𝐵) |
2 | 1 | biimpi 119 |
. . . . . 6
⊢ (𝐴 ≈ 𝐵 → ∃ℎ ℎ:𝐴–1-1-onto→𝐵) |
3 | 2 | ad2antrr 480 |
. . . . 5
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) → ∃ℎ ℎ:𝐴–1-1-onto→𝐵) |
4 | | f1ofn 5408 |
. . . . . . . . . . . 12
⊢ (ℎ:𝐴–1-1-onto→𝐵 → ℎ Fn 𝐴) |
5 | 4 | ad3antlr 485 |
. . . . . . . . . . 11
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → ℎ Fn 𝐴) |
6 | | f1ocnv 5420 |
. . . . . . . . . . . . . 14
⊢ (ℎ:𝐴–1-1-onto→𝐵 → ◡ℎ:𝐵–1-1-onto→𝐴) |
7 | 6 | ad3antlr 485 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → ◡ℎ:𝐵–1-1-onto→𝐴) |
8 | | f1of 5407 |
. . . . . . . . . . . . 13
⊢ (◡ℎ:𝐵–1-1-onto→𝐴 → ◡ℎ:𝐵⟶𝐴) |
9 | 7, 8 | syl 14 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → ◡ℎ:𝐵⟶𝐴) |
10 | | simpr 109 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
11 | 9, 10 | ffvelrnd 5596 |
. . . . . . . . . . 11
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → (◡ℎ‘𝑦) ∈ 𝐴) |
12 | | fvco2 5530 |
. . . . . . . . . . 11
⊢ ((ℎ Fn 𝐴 ∧ (◡ℎ‘𝑦) ∈ 𝐴) → ((𝑔 ∘ ℎ)‘(◡ℎ‘𝑦)) = (𝑔‘(ℎ‘(◡ℎ‘𝑦)))) |
13 | 5, 11, 12 | syl2anc 409 |
. . . . . . . . . 10
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → ((𝑔 ∘ ℎ)‘(◡ℎ‘𝑦)) = (𝑔‘(ℎ‘(◡ℎ‘𝑦)))) |
14 | | fveqeq2 5470 |
. . . . . . . . . . 11
⊢ (𝑥 = (◡ℎ‘𝑦) → (((𝑔 ∘ ℎ)‘𝑥) = 1o ↔ ((𝑔 ∘ ℎ)‘(◡ℎ‘𝑦)) = 1o)) |
15 | | simplr 520 |
. . . . . . . . . . 11
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) |
16 | 14, 15, 11 | rspcdva 2818 |
. . . . . . . . . 10
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → ((𝑔 ∘ ℎ)‘(◡ℎ‘𝑦)) = 1o) |
17 | | simpllr 524 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → ℎ:𝐴–1-1-onto→𝐵) |
18 | | f1ocnvfv2 5719 |
. . . . . . . . . . . 12
⊢ ((ℎ:𝐴–1-1-onto→𝐵 ∧ 𝑦 ∈ 𝐵) → (ℎ‘(◡ℎ‘𝑦)) = 𝑦) |
19 | 17, 18 | sylancom 417 |
. . . . . . . . . . 11
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → (ℎ‘(◡ℎ‘𝑦)) = 𝑦) |
20 | 19 | fveq2d 5465 |
. . . . . . . . . 10
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → (𝑔‘(ℎ‘(◡ℎ‘𝑦))) = (𝑔‘𝑦)) |
21 | 13, 16, 20 | 3eqtr3rd 2196 |
. . . . . . . . 9
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) ∧ 𝑦 ∈ 𝐵) → (𝑔‘𝑦) = 1o) |
22 | 21 | ralrimiva 2527 |
. . . . . . . 8
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o) → ∀𝑦 ∈ 𝐵 (𝑔‘𝑦) = 1o) |
23 | 22 | ex 114 |
. . . . . . 7
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → (∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o → ∀𝑦 ∈ 𝐵 (𝑔‘𝑦) = 1o)) |
24 | 23 | con3d 621 |
. . . . . 6
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → (¬ ∀𝑦 ∈ 𝐵 (𝑔‘𝑦) = 1o → ¬ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o)) |
25 | | fveq1 5460 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑥) = ((𝑔 ∘ ℎ)‘𝑥)) |
26 | 25 | eqeq1d 2163 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑥) = 1o ↔ ((𝑔 ∘ ℎ)‘𝑥) = 1o)) |
27 | 26 | ralbidv 2454 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o)) |
28 | 27 | notbid 657 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ∘ ℎ) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ↔ ¬ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o)) |
29 | 25 | eqeq1d 2163 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑥) = ∅ ↔ ((𝑔 ∘ ℎ)‘𝑥) = ∅)) |
30 | 29 | rexbidv 2455 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ∘ ℎ) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = ∅)) |
31 | 28, 30 | imbi12d 233 |
. . . . . . 7
⊢ (𝑓 = (𝑔 ∘ ℎ) → ((¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅) ↔ (¬ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = ∅))) |
32 | | ismkvmap 7076 |
. . . . . . . . 9
⊢ (𝐴 ∈ Markov → (𝐴 ∈ Markov ↔
∀𝑓 ∈
(2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) |
33 | 32 | ibi 175 |
. . . . . . . 8
⊢ (𝐴 ∈ Markov →
∀𝑓 ∈
(2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)) |
34 | 33 | ad3antlr 485 |
. . . . . . 7
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → ∀𝑓 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)) |
35 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) → 𝑔 ∈ (2o
↑𝑚 𝐵)) |
36 | | 2onn 6457 |
. . . . . . . . . . . . 13
⊢
2o ∈ ω |
37 | | relen 6678 |
. . . . . . . . . . . . . 14
⊢ Rel
≈ |
38 | 37 | brrelex2i 4623 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≈ 𝐵 → 𝐵 ∈ V) |
39 | | elmapg 6595 |
. . . . . . . . . . . . 13
⊢
((2o ∈ ω ∧ 𝐵 ∈ V) → (𝑔 ∈ (2o
↑𝑚 𝐵) ↔ 𝑔:𝐵⟶2o)) |
40 | 36, 38, 39 | sylancr 411 |
. . . . . . . . . . . 12
⊢ (𝐴 ≈ 𝐵 → (𝑔 ∈ (2o
↑𝑚 𝐵) ↔ 𝑔:𝐵⟶2o)) |
41 | 40 | ad2antrr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) → (𝑔 ∈ (2o
↑𝑚 𝐵) ↔ 𝑔:𝐵⟶2o)) |
42 | 35, 41 | mpbid 146 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) → 𝑔:𝐵⟶2o) |
43 | 42 | adantr 274 |
. . . . . . . . 9
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → 𝑔:𝐵⟶2o) |
44 | | f1of 5407 |
. . . . . . . . . 10
⊢ (ℎ:𝐴–1-1-onto→𝐵 → ℎ:𝐴⟶𝐵) |
45 | 44 | adantl 275 |
. . . . . . . . 9
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → ℎ:𝐴⟶𝐵) |
46 | | fco 5328 |
. . . . . . . . 9
⊢ ((𝑔:𝐵⟶2o ∧ ℎ:𝐴⟶𝐵) → (𝑔 ∘ ℎ):𝐴⟶2o) |
47 | 43, 45, 46 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → (𝑔 ∘ ℎ):𝐴⟶2o) |
48 | | simpllr 524 |
. . . . . . . . 9
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → 𝐴 ∈ Markov) |
49 | | elmapg 6595 |
. . . . . . . . 9
⊢
((2o ∈ ω ∧ 𝐴 ∈ Markov) → ((𝑔 ∘ ℎ) ∈ (2o
↑𝑚 𝐴) ↔ (𝑔 ∘ ℎ):𝐴⟶2o)) |
50 | 36, 48, 49 | sylancr 411 |
. . . . . . . 8
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → ((𝑔 ∘ ℎ) ∈ (2o
↑𝑚 𝐴) ↔ (𝑔 ∘ ℎ):𝐴⟶2o)) |
51 | 47, 50 | mpbird 166 |
. . . . . . 7
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → (𝑔 ∘ ℎ) ∈ (2o
↑𝑚 𝐴)) |
52 | 31, 34, 51 | rspcdva 2818 |
. . . . . 6
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → (¬ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = ∅)) |
53 | 4 | ad2antlr 481 |
. . . . . . . . . 10
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ 𝑥 ∈ 𝐴) → ℎ Fn 𝐴) |
54 | | fvco2 5530 |
. . . . . . . . . 10
⊢ ((ℎ Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑔 ∘ ℎ)‘𝑥) = (𝑔‘(ℎ‘𝑥))) |
55 | 53, 54 | sylancom 417 |
. . . . . . . . 9
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝑔 ∘ ℎ)‘𝑥) = (𝑔‘(ℎ‘𝑥))) |
56 | 55 | eqeq1d 2163 |
. . . . . . . 8
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ 𝑥 ∈ 𝐴) → (((𝑔 ∘ ℎ)‘𝑥) = ∅ ↔ (𝑔‘(ℎ‘𝑥)) = ∅)) |
57 | 45 | ffvelrnda 5595 |
. . . . . . . . 9
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ 𝑥 ∈ 𝐴) → (ℎ‘𝑥) ∈ 𝐵) |
58 | | simpr 109 |
. . . . . . . . . 10
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (ℎ‘𝑥)) → 𝑦 = (ℎ‘𝑥)) |
59 | 58 | fveqeq2d 5469 |
. . . . . . . . 9
⊢
((((((𝐴 ≈
𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (ℎ‘𝑥)) → ((𝑔‘𝑦) = ∅ ↔ (𝑔‘(ℎ‘𝑥)) = ∅)) |
60 | 57, 59 | rspcedv 2817 |
. . . . . . . 8
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝑔‘(ℎ‘𝑥)) = ∅ → ∃𝑦 ∈ 𝐵 (𝑔‘𝑦) = ∅)) |
61 | 56, 60 | sylbid 149 |
. . . . . . 7
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) ∧ 𝑥 ∈ 𝐴) → (((𝑔 ∘ ℎ)‘𝑥) = ∅ → ∃𝑦 ∈ 𝐵 (𝑔‘𝑦) = ∅)) |
62 | 61 | rexlimdva 2571 |
. . . . . 6
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → (∃𝑥 ∈ 𝐴 ((𝑔 ∘ ℎ)‘𝑥) = ∅ → ∃𝑦 ∈ 𝐵 (𝑔‘𝑦) = ∅)) |
63 | 24, 52, 62 | 3syld 57 |
. . . . 5
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) ∧ ℎ:𝐴–1-1-onto→𝐵) → (¬ ∀𝑦 ∈ 𝐵 (𝑔‘𝑦) = 1o → ∃𝑦 ∈ 𝐵 (𝑔‘𝑦) = ∅)) |
64 | 3, 63 | exlimddv 1875 |
. . . 4
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) ∧ 𝑔 ∈ (2o
↑𝑚 𝐵)) → (¬ ∀𝑦 ∈ 𝐵 (𝑔‘𝑦) = 1o → ∃𝑦 ∈ 𝐵 (𝑔‘𝑦) = ∅)) |
65 | 64 | ralrimiva 2527 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) → ∀𝑔 ∈ (2o
↑𝑚 𝐵)(¬ ∀𝑦 ∈ 𝐵 (𝑔‘𝑦) = 1o → ∃𝑦 ∈ 𝐵 (𝑔‘𝑦) = ∅)) |
66 | | ismkvmap 7076 |
. . . . 5
⊢ (𝐵 ∈ V → (𝐵 ∈ Markov ↔
∀𝑔 ∈
(2o ↑𝑚 𝐵)(¬ ∀𝑦 ∈ 𝐵 (𝑔‘𝑦) = 1o → ∃𝑦 ∈ 𝐵 (𝑔‘𝑦) = ∅))) |
67 | 38, 66 | syl 14 |
. . . 4
⊢ (𝐴 ≈ 𝐵 → (𝐵 ∈ Markov ↔ ∀𝑔 ∈ (2o
↑𝑚 𝐵)(¬ ∀𝑦 ∈ 𝐵 (𝑔‘𝑦) = 1o → ∃𝑦 ∈ 𝐵 (𝑔‘𝑦) = ∅))) |
68 | 67 | adantr 274 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) → (𝐵 ∈ Markov ↔ ∀𝑔 ∈ (2o
↑𝑚 𝐵)(¬ ∀𝑦 ∈ 𝐵 (𝑔‘𝑦) = 1o → ∃𝑦 ∈ 𝐵 (𝑔‘𝑦) = ∅))) |
69 | 65, 68 | mpbird 166 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Markov) → 𝐵 ∈ Markov) |
70 | 69 | ex 114 |
1
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Markov → 𝐵 ∈ Markov)) |