Metamath Proof Explorer

Theorem domen

Description: Dominance in terms of equinumerosity. Example 1 of Enderton p. 146. (Contributed by NM, 15-Jun-1998)

Ref Expression
Hypothesis bren.1 ⊢ 𝐵 ∈ V
Assertion domen ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 bren.1 ⊢ 𝐵 ∈ V
2 1 brdom ⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
3 vex ⊢ 𝑓 ∈ V
4 3 f11o ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ∃ 𝑥 ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
5 4 exbii ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ∃ 𝑓 ∃ 𝑥 ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
6 excom ⊢ ( ∃ 𝑓 ∃ 𝑥 ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
7 5 6 bitri ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ∃ 𝑥 ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
8 bren ⊢ ( 𝐴 ≈ 𝑥 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑥 )
9 8 anbi1i ⊢ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
10 19.41v ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
11 9 10 bitr4i ⊢ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
12 11 exbii ⊢ ( ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
13 7 12 bitr4i ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
14 2 13 bitri ⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )