Metamath Proof Explorer

Theorem brdom4

Description: An equivalence to a dominance relation. (Contributed by NM, 28-Mar-2007) (Revised by NM, 16-Jun-2017)

Ref Expression
Hypothesis brdom3.2 ⊢ 𝐵 ∈ V
Assertion brdom4 ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )

Proof

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