Step | Hyp | Ref
| Expression |
1 | | brdomi 8531 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
2 | | reldom 8526 |
. . 3
⊢ Rel
≼ |
3 | 2 | brrelex2i 5571 |
. 2
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
4 | | vex 3411 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
5 | | f1stres 7710 |
. . . . . . . . 9
⊢
(1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})⟶(𝐵 ∖ ran 𝑓) |
6 | | difexg 5190 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → (𝐵 ∖ ran 𝑓) ∈ V) |
7 | 6 | adantl 486 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ ran 𝑓) ∈ V) |
8 | | snex 5293 |
. . . . . . . . . 10
⊢
{𝒫 ∪ ran 𝐴} ∈ V |
9 | | xpexg 7464 |
. . . . . . . . . 10
⊢ (((𝐵 ∖ ran 𝑓) ∈ V ∧ {𝒫 ∪ ran 𝐴} ∈ V) → ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}) ∈ V) |
10 | 7, 8, 9 | sylancl 590 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}) ∈ V) |
11 | | fex2 7636 |
. . . . . . . . 9
⊢
(((1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})⟶(𝐵 ∖ ran 𝑓) ∧ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}) ∈ V ∧ (𝐵 ∖ ran 𝑓) ∈ V) → (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})) ∈ V) |
12 | 5, 10, 7, 11 | mp3an2i 1464 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})) ∈ V) |
13 | | unexg 7463 |
. . . . . . . 8
⊢ ((𝑓 ∈ V ∧ (1st
↾ ((𝐵 ∖ ran
𝑓) × {𝒫 ∪ ran 𝐴})) ∈ V) → (𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
14 | 4, 12, 13 | sylancr 591 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
15 | | cnvexg 7627 |
. . . . . . 7
⊢ ((𝑓 ∪ (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V → ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
17 | | rnexg 7607 |
. . . . . 6
⊢ (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V → ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) |
19 | | simpl 487 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝑓:𝐴–1-1→𝐵) |
20 | | f1dm 6557 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1→𝐵 → dom 𝑓 = 𝐴) |
21 | 4 | dmex 7614 |
. . . . . . . . . 10
⊢ dom 𝑓 ∈ V |
22 | 20, 21 | eqeltrrdi 2860 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1→𝐵 → 𝐴 ∈ V) |
23 | 22 | adantr 485 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐴 ∈ V) |
24 | | simpr 489 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐵 ∈ V) |
25 | | eqid 2759 |
. . . . . . . . 9
⊢ ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) = ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) |
26 | 25 | domss2 8690 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∘ 𝑓) = ( I ↾ 𝐴))) |
27 | 19, 23, 24, 26 | syl3anc 1369 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ (◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∘ 𝑓) = ( I ↾ 𝐴))) |
28 | 27 | simp2d 1141 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) |
29 | 27 | simp1d 1140 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) |
30 | | f1oen3g 8536 |
. . . . . . 7
⊢ ((◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V ∧ ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) → 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) |
31 | 16, 29, 30 | syl2anc 588 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) |
32 | 28, 31 | jca 516 |
. . . . 5
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))))) |
33 | | sseq2 3914 |
. . . . . 6
⊢ (𝑥 = ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))))) |
34 | | breq2 5029 |
. . . . . 6
⊢ (𝑥 = ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) → (𝐵 ≈ 𝑥 ↔ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))))) |
35 | 33, 34 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) → ((𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥) ↔ (𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))))) |
36 | 18, 32, 35 | spcedv 3515 |
. . . 4
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥)) |
37 | 36 | ex 417 |
. . 3
⊢ (𝑓:𝐴–1-1→𝐵 → (𝐵 ∈ V → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥))) |
38 | 37 | exlimiv 1932 |
. 2
⊢
(∃𝑓 𝑓:𝐴–1-1→𝐵 → (𝐵 ∈ V → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥))) |
39 | 1, 3, 38 | sylc 65 |
1
⊢ (𝐴 ≼ 𝐵 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥)) |