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

Metamath Proof Explorer

Theorem brwdom3

Description: Condition for weak dominance with a condition reminiscent of wdomd . (Contributed by Stefan O'Rear, 13-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion brwdom3 ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ V )
2 elex ⊢ ( 𝑌 ∈ 𝑊 → 𝑌 ∈ V )
3 brwdom2 ⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑧 ∈ 𝒫 𝑌 ∃ 𝑓 𝑓 : 𝑧 –onto→ 𝑋 ) )
4 3 adantl ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑧 ∈ 𝒫 𝑌 ∃ 𝑓 𝑓 : 𝑧 –onto→ 𝑋 ) )
5 dffo3 ⊢ ( 𝑓 : 𝑧 –onto→ 𝑋 ↔ ( 𝑓 : 𝑧 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑧 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
6 5 simprbi ⊢ ( 𝑓 : 𝑧 –onto→ 𝑋 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑧 𝑥 = ( 𝑓 ‘ 𝑦 ) )
7 elpwi ⊢ ( 𝑧 ∈ 𝒫 𝑌 → 𝑧 ⊆ 𝑌 )
8 ssrexv ⊢ ( 𝑧 ⊆ 𝑌 → ( ∃ 𝑦 ∈ 𝑧 𝑥 = ( 𝑓 ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
9 7 8 syl ⊢ ( 𝑧 ∈ 𝒫 𝑌 → ( ∃ 𝑦 ∈ 𝑧 𝑥 = ( 𝑓 ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
10 9 adantl ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑧 ∈ 𝒫 𝑌 ) → ( ∃ 𝑦 ∈ 𝑧 𝑥 = ( 𝑓 ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
11 10 ralimdv ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑧 ∈ 𝒫 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑧 𝑥 = ( 𝑓 ‘ 𝑦 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
12 6 11 syl5 ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑧 ∈ 𝒫 𝑌 ) → ( 𝑓 : 𝑧 –onto→ 𝑋 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
13 12 eximdv ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑧 ∈ 𝒫 𝑌 ) → ( ∃ 𝑓 𝑓 : 𝑧 –onto→ 𝑋 → ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
14 13 rexlimdva ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ∃ 𝑧 ∈ 𝒫 𝑌 ∃ 𝑓 𝑓 : 𝑧 –onto→ 𝑋 → ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
15 4 14 sylbid ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ≼* 𝑌 → ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
16 simpll ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) → 𝑋 ∈ V )
17 simplr ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) → 𝑌 ∈ V )
18 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( 𝑓 ‘ 𝑦 ) ↔ 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
19 18 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑌 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
20 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑤 ) )
21 20 eqeq2d ⊢ ( 𝑦 = 𝑤 → ( 𝑧 = ( 𝑓 ‘ 𝑦 ) ↔ 𝑧 = ( 𝑓 ‘ 𝑤 ) ) )
22 21 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝑌 𝑧 = ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑤 ∈ 𝑌 𝑧 = ( 𝑓 ‘ 𝑤 ) )
23 19 22 bitrdi ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑤 ∈ 𝑌 𝑧 = ( 𝑓 ‘ 𝑤 ) ) )
24 23 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 = ( 𝑓 ‘ 𝑤 ) )
25 24 biimpi ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) → ∀ 𝑧 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 = ( 𝑓 ‘ 𝑤 ) )
26 25 adantl ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) → ∀ 𝑧 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 = ( 𝑓 ‘ 𝑤 ) )
27 26 r19.21bi ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑋 ) → ∃ 𝑤 ∈ 𝑌 𝑧 = ( 𝑓 ‘ 𝑤 ) )
28 16 17 27 wdom2d ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) → 𝑋 ≼* 𝑌 )
29 28 ex ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) → 𝑋 ≼* 𝑌 ) )
30 29 exlimdv ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) → 𝑋 ≼* 𝑌 ) )
31 15 30 impbid ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
32 1 2 31 syl2an ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )