| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | brdomi 9000 | . 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) | 
| 2 |  | reldom 8992 | . . 3
⊢ Rel
≼ | 
| 3 | 2 | brrelex2i 5741 | . 2
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) | 
| 4 |  | vex 3483 | . . . . . . . 8
⊢ 𝑓 ∈ V | 
| 5 |  | f1stres 8039 | . . . . . . . . 9
⊢
(1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})⟶(𝐵 ∖ ran 𝑓) | 
| 6 |  | difexg 5328 | . . . . . . . . . . 11
⊢ (𝐵 ∈ V → (𝐵 ∖ ran 𝑓) ∈ V) | 
| 7 | 6 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ ran 𝑓) ∈ V) | 
| 8 |  | snex 5435 | . . . . . . . . . 10
⊢
{𝒫 ∪ ran 𝐴} ∈ V | 
| 9 |  | xpexg 7771 | . . . . . . . . . 10
⊢ (((𝐵 ∖ ran 𝑓) ∈ V ∧ {𝒫 ∪ ran 𝐴} ∈ V) → ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}) ∈ V) | 
| 10 | 7, 8, 9 | sylancl 586 | . . . . . . . . 9
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}) ∈ V) | 
| 11 |  | fex2 7959 | . . . . . . . . 9
⊢
(((1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})⟶(𝐵 ∖ ran 𝑓) ∧ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}) ∈ V ∧ (𝐵 ∖ ran 𝑓) ∈ V) → (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})) ∈ V) | 
| 12 | 5, 10, 7, 11 | mp3an2i 1467 | . . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})) ∈ V) | 
| 13 |  | unexg 7764 | . . . . . . . 8
⊢ ((𝑓 ∈ V ∧ (1st
↾ ((𝐵 ∖ ran
𝑓) × {𝒫 ∪ ran 𝐴})) ∈ V) → (𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) | 
| 14 | 4, 12, 13 | sylancr 587 | . . . . . . 7
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) | 
| 15 |  | cnvexg 7947 | . . . . . . 7
⊢ ((𝑓 ∪ (1st ↾
((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V → ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) | 
| 16 | 14, 15 | syl 17 | . . . . . 6
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V) | 
| 17 |  | rnexg 7925 | . . . . . 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 482 | . . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝑓:𝐴–1-1→𝐵) | 
| 20 |  | f1dm 6807 | . . . . . . . . . 10
⊢ (𝑓:𝐴–1-1→𝐵 → dom 𝑓 = 𝐴) | 
| 21 | 4 | dmex 7932 | . . . . . . . . . 10
⊢ dom 𝑓 ∈ V | 
| 22 | 20, 21 | eqeltrrdi 2849 | . . . . . . . . 9
⊢ (𝑓:𝐴–1-1→𝐵 → 𝐴 ∈ V) | 
| 23 | 22 | adantr 480 | . . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐴 ∈ V) | 
| 24 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐵 ∈ V) | 
| 25 |  | eqid 2736 | . . . . . . . . 9
⊢ ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) = ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) | 
| 26 | 25 | domss2 9177 | . . . . . . . 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 1372 | . . . . . . 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 1143 | . . . . . 6
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) | 
| 29 | 27 | simp1d 1142 | . . . . . . 7
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) | 
| 30 |  | f1oen3g 9008 | . . . . . . 7
⊢ ((◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∈ V ∧ ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→ran
◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) → 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) | 
| 31 | 16, 29, 30 | syl2anc 584 | . . . . . 6
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))) | 
| 32 | 28, 31 | jca 511 | . . . . 5
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → (𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))))) | 
| 33 |  | sseq2 4009 | . . . . . 6
⊢ (𝑥 = ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))))) | 
| 34 |  | breq2 5146 | . . . . . 6
⊢ (𝑥 = ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) → (𝐵 ≈ 𝑥 ↔ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))))) | 
| 35 | 33, 34 | anbi12d 632 | . . . . 5
⊢ (𝑥 = ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) → ((𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥) ↔ (𝐴 ⊆ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴}))) ∧ 𝐵 ≈ ran ◡(𝑓 ∪ (1st ↾ ((𝐵 ∖ ran 𝑓) × {𝒫 ∪ ran 𝐴})))))) | 
| 36 | 18, 32, 35 | spcedv 3597 | . . . 4
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥)) | 
| 37 | 36 | ex 412 | . . 3
⊢ (𝑓:𝐴–1-1→𝐵 → (𝐵 ∈ V → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥))) | 
| 38 | 37 | exlimiv 1929 | . 2
⊢
(∃𝑓 𝑓:𝐴–1-1→𝐵 → (𝐵 ∈ V → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥))) | 
| 39 | 1, 3, 38 | sylc 65 | 1
⊢ (𝐴 ≼ 𝐵 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥)) |