Step | Hyp | Ref
| Expression |
1 | | brdomi 7852 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
2 | | reldom 7847 |
. . 3
⊢ Rel
≼ |
3 | 2 | brrelex2i 5083 |
. 2
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
4 | | vex 3176 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
5 | | f1stres 7081 |
. . . . . . . . . 10
⊢
(1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})⟶(𝐵 ∖ ran 𝑓) |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})⟶(𝐵 ∖ ran 𝑓)) |
7 | | difexg 4735 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → (𝐵 ∖ ran 𝑓) ∈ V) |
8 | 7 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ ran 𝑓) ∈ V) |
9 | | snex 4835 |
. . . . . . . . . 10
⊢
{𝒫 ∪ ran 𝐴} ∈ V |
10 | | xpexg 6858 |
. . . . . . . . . 10
⊢ (((𝐵 ∖ ran 𝑓) ∈ V ∧ {𝒫 ∪ ran 𝐴} ∈ V) → ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}) ∈ V) |
11 | 8, 9, 10 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}) ∈ V) |
12 | | fex2 7014 |
. . . . . . . . 9
⊢
(((1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})⟶(𝐵 ∖ ran 𝑓) ∧ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}) ∈ V ∧ (𝐵 ∖ ran 𝑓) ∈ V) → (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})) ∈ V) |
13 | 6, 11, 8, 12 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})) ∈ V) |
14 | | unexg 6857 |
. . . . . . . 8
⊢ ((𝑓 ∈ V ∧ (1st
↾ ((𝐵 ∖ ran
𝑓) × {𝒫 ∪ ran 𝐴})) ∈ V) → (𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
15 | 4, 13, 14 | sylancr 694 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
16 | | cnvexg 7005 |
. . . . . . 7
⊢ ((𝑓 ∪ (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V → ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
18 | | rnexg 6990 |
. . . . . 6
⊢ (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V → ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
20 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝑓:𝐴–1-1→𝐵) |
21 | | f1dm 6018 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1→𝐵 → dom 𝑓 = 𝐴) |
22 | 4 | dmex 6991 |
. . . . . . . . . 10
⊢ dom 𝑓 ∈ V |
23 | 21, 22 | syl6eqelr 2697 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1→𝐵 → 𝐴 ∈ V) |
24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐴 ∈ V) |
25 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐵 ∈ V) |
26 | | eqid 2610 |
. . . . . . . . 9
⊢ ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) = ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) |
27 | 26 | domss2 8004 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∘ 𝑓) = ( I ↾ 𝐴))) |
28 | 20, 24, 25, 27 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∘ 𝑓) = ( I ↾ 𝐴))) |
29 | 28 | simp2d 1067 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) |
30 | 28 | simp1d 1066 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) |
31 | | f1oen3g 7857 |
. . . . . . 7
⊢ ((◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V ∧ ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) → 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) |
32 | 17, 30, 31 | syl2anc 691 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) |
33 | 29, 32 | jca 553 |
. . . . 5
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))))) |
34 | | sseq2 3590 |
. . . . . . 7
⊢ (𝑥 = ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))))) |
35 | | breq2 4587 |
. . . . . . 7
⊢ (𝑥 = ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) → (𝐵 ≈ 𝑥 ↔ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))))) |
36 | 34, 35 | anbi12d 743 |
. . . . . 6
⊢ (𝑥 = ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) → ((𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥) ↔ (𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))))) |
37 | 36 | spcegv 3267 |
. . . . 5
⊢ (ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V → ((𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥))) |
38 | 19, 33, 37 | sylc 63 |
. . . 4
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥)) |
39 | 38 | ex 449 |
. . 3
⊢ (𝑓:𝐴–1-1→𝐵 → (𝐵 ∈ V → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥))) |
40 | 39 | exlimiv 1845 |
. 2
⊢
(∃𝑓 𝑓:𝐴–1-1→𝐵 → (𝐵 ∈ V → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥))) |
41 | 1, 3, 40 | sylc 63 |
1
⊢ (𝐴 ≼ 𝐵 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥)) |