Step | Hyp | Ref
| Expression |
1 | | relwdom 8354 |
. . . . 5
⊢ Rel
≼* |
2 | 1 | brrelex2i 5083 |
. . . 4
⊢ (𝑌 ≼* 𝑍 → 𝑍 ∈ V) |
3 | 2 | adantl 481 |
. . 3
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → 𝑍 ∈ V) |
4 | | 0wdom 8358 |
. . . 4
⊢ (𝑍 ∈ V → ∅
≼* 𝑍) |
5 | | breq1 4586 |
. . . 4
⊢ (𝑋 = ∅ → (𝑋 ≼* 𝑍 ↔ ∅
≼* 𝑍)) |
6 | 4, 5 | syl5ibrcom 236 |
. . 3
⊢ (𝑍 ∈ V → (𝑋 = ∅ → 𝑋 ≼* 𝑍)) |
7 | 3, 6 | syl 17 |
. 2
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → (𝑋 = ∅ → 𝑋 ≼* 𝑍)) |
8 | | simpll 786 |
. . . . 5
⊢ (((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) → 𝑋 ≼* 𝑌) |
9 | | brwdomn0 8357 |
. . . . . 6
⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)) |
10 | 9 | adantl 481 |
. . . . 5
⊢ (((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)) |
11 | 8, 10 | mpbid 221 |
. . . 4
⊢ (((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) → ∃𝑧 𝑧:𝑌–onto→𝑋) |
12 | | simpllr 795 |
. . . . . 6
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ 𝑧:𝑌–onto→𝑋) → 𝑌 ≼* 𝑍) |
13 | | simplr 788 |
. . . . . . . 8
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ 𝑧:𝑌–onto→𝑋) → 𝑋 ≠ ∅) |
14 | | dm0rn0 5263 |
. . . . . . . . . . . 12
⊢ (dom
𝑧 = ∅ ↔ ran
𝑧 =
∅) |
15 | 14 | necon3bii 2834 |
. . . . . . . . . . 11
⊢ (dom
𝑧 ≠ ∅ ↔ ran
𝑧 ≠
∅) |
16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑧:𝑌–onto→𝑋 → (dom 𝑧 ≠ ∅ ↔ ran 𝑧 ≠ ∅)) |
17 | | fof 6028 |
. . . . . . . . . . . 12
⊢ (𝑧:𝑌–onto→𝑋 → 𝑧:𝑌⟶𝑋) |
18 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝑧:𝑌⟶𝑋 → dom 𝑧 = 𝑌) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧:𝑌–onto→𝑋 → dom 𝑧 = 𝑌) |
20 | 19 | neeq1d 2841 |
. . . . . . . . . 10
⊢ (𝑧:𝑌–onto→𝑋 → (dom 𝑧 ≠ ∅ ↔ 𝑌 ≠ ∅)) |
21 | | forn 6031 |
. . . . . . . . . . 11
⊢ (𝑧:𝑌–onto→𝑋 → ran 𝑧 = 𝑋) |
22 | 21 | neeq1d 2841 |
. . . . . . . . . 10
⊢ (𝑧:𝑌–onto→𝑋 → (ran 𝑧 ≠ ∅ ↔ 𝑋 ≠ ∅)) |
23 | 16, 20, 22 | 3bitr3rd 298 |
. . . . . . . . 9
⊢ (𝑧:𝑌–onto→𝑋 → (𝑋 ≠ ∅ ↔ 𝑌 ≠ ∅)) |
24 | 23 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ 𝑧:𝑌–onto→𝑋) → (𝑋 ≠ ∅ ↔ 𝑌 ≠ ∅)) |
25 | 13, 24 | mpbid 221 |
. . . . . . 7
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ 𝑧:𝑌–onto→𝑋) → 𝑌 ≠ ∅) |
26 | | brwdomn0 8357 |
. . . . . . 7
⊢ (𝑌 ≠ ∅ → (𝑌 ≼* 𝑍 ↔ ∃𝑦 𝑦:𝑍–onto→𝑌)) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ 𝑧:𝑌–onto→𝑋) → (𝑌 ≼* 𝑍 ↔ ∃𝑦 𝑦:𝑍–onto→𝑌)) |
28 | 12, 27 | mpbid 221 |
. . . . 5
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ 𝑧:𝑌–onto→𝑋) → ∃𝑦 𝑦:𝑍–onto→𝑌) |
29 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
30 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
31 | 29, 30 | coex 7011 |
. . . . . . . . 9
⊢ (𝑧 ∘ 𝑦) ∈ V |
32 | | foco 6038 |
. . . . . . . . 9
⊢ ((𝑧:𝑌–onto→𝑋 ∧ 𝑦:𝑍–onto→𝑌) → (𝑧 ∘ 𝑦):𝑍–onto→𝑋) |
33 | | fowdom 8359 |
. . . . . . . . 9
⊢ (((𝑧 ∘ 𝑦) ∈ V ∧ (𝑧 ∘ 𝑦):𝑍–onto→𝑋) → 𝑋 ≼* 𝑍) |
34 | 31, 32, 33 | sylancr 694 |
. . . . . . . 8
⊢ ((𝑧:𝑌–onto→𝑋 ∧ 𝑦:𝑍–onto→𝑌) → 𝑋 ≼* 𝑍) |
35 | 34 | adantl 481 |
. . . . . . 7
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ (𝑧:𝑌–onto→𝑋 ∧ 𝑦:𝑍–onto→𝑌)) → 𝑋 ≼* 𝑍) |
36 | 35 | expr 641 |
. . . . . 6
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ 𝑧:𝑌–onto→𝑋) → (𝑦:𝑍–onto→𝑌 → 𝑋 ≼* 𝑍)) |
37 | 36 | exlimdv 1848 |
. . . . 5
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ 𝑧:𝑌–onto→𝑋) → (∃𝑦 𝑦:𝑍–onto→𝑌 → 𝑋 ≼* 𝑍)) |
38 | 28, 37 | mpd 15 |
. . . 4
⊢ ((((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) ∧ 𝑧:𝑌–onto→𝑋) → 𝑋 ≼* 𝑍) |
39 | 11, 38 | exlimddv 1850 |
. . 3
⊢ (((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) ∧ 𝑋 ≠ ∅) → 𝑋 ≼* 𝑍) |
40 | 39 | ex 449 |
. 2
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → (𝑋 ≠ ∅ → 𝑋 ≼* 𝑍)) |
41 | 7, 40 | pm2.61dne 2868 |
1
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → 𝑋 ≼* 𝑍) |