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

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