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 ( ( 𝑋𝑉𝑌𝑊 ) → ( 𝑋* 𝑌 ↔ ∃ 𝑓𝑥𝑋𝑦𝑌 𝑥 = ( 𝑓𝑦 ) ) )