This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brdom5

Description: An equivalence to a dominance relation. (Contributed by NM, 29-Mar-2007)

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

Proof

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 ⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )