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