Metamath Proof Explorer


Theorem brdom3

Description: Equivalence to a dominance relation. (Contributed by NM, 27-Mar-2007)

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

Proof

Step Hyp Ref Expression
1 brdom3.2 𝐵 ∈ V
2 reldom Rel ≼
3 2 brrelex1i ( 𝐴𝐵𝐴 ∈ V )
4 0sdomg ( 𝐴 ∈ V → ( ∅ ≺ 𝐴𝐴 ≠ ∅ ) )
5 3 4 syl ( 𝐴𝐵 → ( ∅ ≺ 𝐴𝐴 ≠ ∅ ) )
6 df-ne ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
7 5 6 bitrdi ( 𝐴𝐵 → ( ∅ ≺ 𝐴 ↔ ¬ 𝐴 = ∅ ) )
8 7 biimpar ( ( 𝐴𝐵 ∧ ¬ 𝐴 = ∅ ) → ∅ ≺ 𝐴 )
9 fodomr ( ( ∅ ≺ 𝐴𝐴𝐵 ) → ∃ 𝑓 𝑓 : 𝐵onto𝐴 )
10 9 ancoms ( ( 𝐴𝐵 ∧ ∅ ≺ 𝐴 ) → ∃ 𝑓 𝑓 : 𝐵onto𝐴 )
11 8 10 syldan ( ( 𝐴𝐵 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑓 𝑓 : 𝐵onto𝐴 )
12 pm5.6 ( ( ( 𝐴𝐵 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑓 𝑓 : 𝐵onto𝐴 ) ↔ ( 𝐴𝐵 → ( 𝐴 = ∅ ∨ ∃ 𝑓 𝑓 : 𝐵onto𝐴 ) ) )
13 11 12 mpbi ( 𝐴𝐵 → ( 𝐴 = ∅ ∨ ∃ 𝑓 𝑓 : 𝐵onto𝐴 ) )
14 br0 ¬ 𝑥𝑦
15 14 nex ¬ ∃ 𝑦 𝑥𝑦
16 exmo ( ∃ 𝑦 𝑥𝑦 ∨ ∃* 𝑦 𝑥𝑦 )
17 15 16 mtpor ∃* 𝑦 𝑥𝑦
18 17 ax-gen 𝑥 ∃* 𝑦 𝑥𝑦
19 rzal ( 𝐴 = ∅ → ∀ 𝑥𝐴𝑦𝐵 𝑦𝑥 )
20 0ex ∅ ∈ V
21 breq ( 𝑓 = ∅ → ( 𝑥 𝑓 𝑦𝑥𝑦 ) )
22 21 mobidv ( 𝑓 = ∅ → ( ∃* 𝑦 𝑥 𝑓 𝑦 ↔ ∃* 𝑦 𝑥𝑦 ) )
23 22 albidv ( 𝑓 = ∅ → ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ↔ ∀ 𝑥 ∃* 𝑦 𝑥𝑦 ) )
24 breq ( 𝑓 = ∅ → ( 𝑦 𝑓 𝑥𝑦𝑥 ) )
25 24 rexbidv ( 𝑓 = ∅ → ( ∃ 𝑦𝐵 𝑦 𝑓 𝑥 ↔ ∃ 𝑦𝐵 𝑦𝑥 ) )
26 25 ralbidv ( 𝑓 = ∅ → ( ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ↔ ∀ 𝑥𝐴𝑦𝐵 𝑦𝑥 ) )
27 23 26 anbi12d ( 𝑓 = ∅ → ( ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) ↔ ( ∀ 𝑥 ∃* 𝑦 𝑥𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦𝑥 ) ) )
28 20 27 spcev ( ( ∀ 𝑥 ∃* 𝑦 𝑥𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦𝑥 ) → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) )
29 18 19 28 sylancr ( 𝐴 = ∅ → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) )
30 fofun ( 𝑓 : 𝐵onto𝐴 → Fun 𝑓 )
31 dffun6 ( Fun 𝑓 ↔ ( Rel 𝑓 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ) )
32 31 simprbi ( Fun 𝑓 → ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 )
33 30 32 syl ( 𝑓 : 𝐵onto𝐴 → ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 )
34 dffo4 ( 𝑓 : 𝐵onto𝐴 ↔ ( 𝑓 : 𝐵𝐴 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) )
35 34 simprbi ( 𝑓 : 𝐵onto𝐴 → ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 )
36 33 35 jca ( 𝑓 : 𝐵onto𝐴 → ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) )
37 36 eximi ( ∃ 𝑓 𝑓 : 𝐵onto𝐴 → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) )
38 29 37 jaoi ( ( 𝐴 = ∅ ∨ ∃ 𝑓 𝑓 : 𝐵onto𝐴 ) → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) )
39 13 38 syl ( 𝐴𝐵 → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) )
40 inss1 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝑓
41 40 ssbri ( 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦𝑥 𝑓 𝑦 )
42 41 moimi ( ∃* 𝑦 𝑥 𝑓 𝑦 → ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 )
43 42 alimi ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 → ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 )
44 relinxp Rel ( 𝑓 ∩ ( 𝐵 × 𝐴 ) )
45 dffun6 ( Fun ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ↔ ( Rel ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 ) )
46 44 45 mpbiran ( Fun ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ↔ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 )
47 43 46 sylibr ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 → Fun ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) )
48 47 funfnd ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 → ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) Fn dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) )
49 rninxp ( ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ↔ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 )
50 49 biimpri ( ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 → ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 )
51 48 50 anim12i ( ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) → ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) Fn dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ) )
52 df-fo ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) : dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) –onto𝐴 ↔ ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) Fn dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ) )
53 51 52 sylibr ( ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) → ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) : dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) –onto𝐴 )
54 vex 𝑓 ∈ V
55 54 inex1 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∈ V
56 55 dmex dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∈ V
57 56 fodom ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) : dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) –onto𝐴𝐴 ≼ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) )
58 inss2 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ ( 𝐵 × 𝐴 )
59 dmss ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ ( 𝐵 × 𝐴 ) → dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ dom ( 𝐵 × 𝐴 ) )
60 58 59 ax-mp dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ dom ( 𝐵 × 𝐴 )
61 dmxpss dom ( 𝐵 × 𝐴 ) ⊆ 𝐵
62 60 61 sstri dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝐵
63 ssdomg ( 𝐵 ∈ V → ( dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝐵 → dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ≼ 𝐵 ) )
64 1 62 63 mp2 dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ≼ 𝐵
65 domtr ( ( 𝐴 ≼ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ≼ 𝐵 ) → 𝐴𝐵 )
66 64 65 mpan2 ( 𝐴 ≼ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) → 𝐴𝐵 )
67 53 57 66 3syl ( ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) → 𝐴𝐵 )
68 67 exlimiv ( ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) → 𝐴𝐵 )
69 39 68 impbii ( 𝐴𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑦 𝑓 𝑥 ) )