Step |
Hyp |
Ref |
Expression |
1 |
|
brdom3.2 |
⊢ 𝐵 ∈ V |
2 |
1
|
brdom3 |
⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) ) |
3 |
|
alral |
⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 → ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ) |
4 |
3
|
anim1i |
⊢ ( ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) ) |
5 |
4
|
eximi |
⊢ ( ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) ) |
6 |
2 5
|
sylbi |
⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) ) |
7 |
|
inss2 |
⊢ ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ ( 𝐵 × 𝐴 ) |
8 |
|
dmss |
⊢ ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ ( 𝐵 × 𝐴 ) → dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ dom ( 𝐵 × 𝐴 ) ) |
9 |
7 8
|
ax-mp |
⊢ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ dom ( 𝐵 × 𝐴 ) |
10 |
|
dmxpss |
⊢ dom ( 𝐵 × 𝐴 ) ⊆ 𝐵 |
11 |
9 10
|
sstri |
⊢ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝐵 |
12 |
11
|
sseli |
⊢ ( 𝑥 ∈ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) → 𝑥 ∈ 𝐵 ) |
13 |
|
inss1 |
⊢ ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝑓 |
14 |
13
|
ssbri |
⊢ ( 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 → 𝑥 𝑓 𝑦 ) |
15 |
14
|
moimi |
⊢ ( ∃* 𝑦 𝑥 𝑓 𝑦 → ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 ) |
16 |
12 15
|
imim12i |
⊢ ( ( 𝑥 ∈ 𝐵 → ∃* 𝑦 𝑥 𝑓 𝑦 ) → ( 𝑥 ∈ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) → ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 ) ) |
17 |
16
|
ralimi2 |
⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 → ∀ 𝑥 ∈ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 ) |
18 |
|
relinxp |
⊢ Rel ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) |
19 |
17 18
|
jctil |
⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 → ( Rel ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ∀ 𝑥 ∈ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 ) ) |
20 |
|
dffun7 |
⊢ ( Fun ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ↔ ( Rel ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ∀ 𝑥 ∈ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 ) ) |
21 |
19 20
|
sylibr |
⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 → Fun ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ) |
22 |
21
|
funfnd |
⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 → ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) Fn dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ) |
23 |
|
rninxp |
⊢ ( ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) |
24 |
23
|
biimpri |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 → ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ) |
25 |
22 24
|
anim12i |
⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) Fn dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ) ) |
26 |
|
df-fo |
⊢ ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) : dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) –onto→ 𝐴 ↔ ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) Fn dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ) ) |
27 |
25 26
|
sylibr |
⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) : dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) –onto→ 𝐴 ) |
28 |
|
vex |
⊢ 𝑓 ∈ V |
29 |
28
|
inex1 |
⊢ ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∈ V |
30 |
29
|
dmex |
⊢ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∈ V |
31 |
30
|
fodom |
⊢ ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) : dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) –onto→ 𝐴 → 𝐴 ≼ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ) |
32 |
|
ssdomg |
⊢ ( 𝐵 ∈ V → ( dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝐵 → dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ≼ 𝐵 ) ) |
33 |
1 11 32
|
mp2 |
⊢ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ≼ 𝐵 |
34 |
|
domtr |
⊢ ( ( 𝐴 ≼ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ≼ 𝐵 ) → 𝐴 ≼ 𝐵 ) |
35 |
33 34
|
mpan2 |
⊢ ( 𝐴 ≼ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) → 𝐴 ≼ 𝐵 ) |
36 |
27 31 35
|
3syl |
⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → 𝐴 ≼ 𝐵 ) |
37 |
36
|
exlimiv |
⊢ ( ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → 𝐴 ≼ 𝐵 ) |
38 |
6 37
|
impbii |
⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) ) |