Metamath Proof Explorer

Theorem brwdom2

Description: Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Assertion brwdom2 ( 𝑌 ∈ 𝑉 → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝑌 ∈ 𝑉 → 𝑌 ∈ V )
2 0wdom ⊢ ( 𝑌 ∈ V → ∅ ≼* 𝑌 )
3 breq1 ⊢ ( 𝑋 = ∅ → ( 𝑋 ≼* 𝑌 ↔ ∅ ≼* 𝑌 ) )
4 2 3 syl5ibrcom ⊢ ( 𝑌 ∈ V → ( 𝑋 = ∅ → 𝑋 ≼* 𝑌 ) )
5 4 imp ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 = ∅ ) → 𝑋 ≼* 𝑌 )
6 0elpw ⊢ ∅ ∈ 𝒫 𝑌
7 f1o0 ⊢ ∅ : ∅ –1-1-onto→ ∅
8 f1ofo ⊢ ( ∅ : ∅ –1-1-onto→ ∅ → ∅ : ∅ –onto→ ∅ )
9 0ex ⊢ ∅ ∈ V
10 foeq1 ⊢ ( 𝑧 = ∅ → ( 𝑧 : ∅ –onto→ ∅ ↔ ∅ : ∅ –onto→ ∅ ) )
11 9 10 spcev ⊢ ( ∅ : ∅ –onto→ ∅ → ∃ 𝑧 𝑧 : ∅ –onto→ ∅ )
12 7 8 11 mp2b ⊢ ∃ 𝑧 𝑧 : ∅ –onto→ ∅
13 foeq2 ⊢ ( 𝑦 = ∅ → ( 𝑧 : 𝑦 –onto→ ∅ ↔ 𝑧 : ∅ –onto→ ∅ ) )
14 13 exbidv ⊢ ( 𝑦 = ∅ → ( ∃ 𝑧 𝑧 : 𝑦 –onto→ ∅ ↔ ∃ 𝑧 𝑧 : ∅ –onto→ ∅ ) )
15 14 rspcev ⊢ ( ( ∅ ∈ 𝒫 𝑌 ∧ ∃ 𝑧 𝑧 : ∅ –onto→ ∅ ) → ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ ∅ )
16 6 12 15 mp2an ⊢ ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ ∅
17 foeq3 ⊢ ( 𝑋 = ∅ → ( 𝑧 : 𝑦 –onto→ 𝑋 ↔ 𝑧 : 𝑦 –onto→ ∅ ) )
18 17 exbidv ⊢ ( 𝑋 = ∅ → ( ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ↔ ∃ 𝑧 𝑧 : 𝑦 –onto→ ∅ ) )
19 18 rexbidv ⊢ ( 𝑋 = ∅ → ( ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ↔ ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ ∅ ) )
20 16 19 mpbiri ⊢ ( 𝑋 = ∅ → ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 )
21 20 adantl ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 = ∅ ) → ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 )
22 5 21 2thd ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 = ∅ ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) )
23 brwdomn0 ⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 ) )
24 23 adantl ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 ) )
25 foeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 : 𝑌 –onto→ 𝑋 ↔ 𝑧 : 𝑌 –onto→ 𝑋 ) )
26 25 cbvexvw ⊢ ( ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 )
27 pwidg ⊢ ( 𝑌 ∈ V → 𝑌 ∈ 𝒫 𝑌 )
28 27 ad2antrr ⊢ ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝑌 ∈ 𝒫 𝑌 )
29 foeq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑧 : 𝑦 –onto→ 𝑋 ↔ 𝑧 : 𝑌 –onto→ 𝑋 ) )
30 29 exbidv ⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
31 30 rspcev ⊢ ( ( 𝑌 ∈ 𝒫 𝑌 ∧ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) → ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 )
32 28 31 sylancom ⊢ ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) → ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 )
33 32 ex ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 → ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) )
34 26 33 syl5bi ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 → ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) )
35 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝑋 )
36 35 biimpi ⊢ ( 𝑋 ≠ ∅ → ∃ 𝑤 𝑤 ∈ 𝑋 )
37 36 ad2antlr ⊢ ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) → ∃ 𝑤 𝑤 ∈ 𝑋 )
38 vex ⊢ 𝑧 ∈ V
39 difexg ⊢ ( 𝑌 ∈ V → ( 𝑌 ∖ 𝑦 ) ∈ V )
40 snex ⊢ { 𝑤 } ∈ V
41 xpexg ⊢ ( ( ( 𝑌 ∖ 𝑦 ) ∈ V ∧ { 𝑤 } ∈ V ) → ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ∈ V )
42 39 40 41 sylancl ⊢ ( 𝑌 ∈ V → ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ∈ V )
43 unexg ⊢ ( ( 𝑧 ∈ V ∧ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ∈ V ) → ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) ∈ V )
44 38 42 43 sylancr ⊢ ( 𝑌 ∈ V → ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) ∈ V )
45 44 adantr ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) → ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) ∈ V )
46 45 ad2antrr ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) ∈ V )
47 fofn ⊢ ( 𝑧 : 𝑦 –onto→ 𝑋 → 𝑧 Fn 𝑦 )
48 47 adantl ⊢ ( ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) → 𝑧 Fn 𝑦 )
49 48 ad2antlr ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝑧 Fn 𝑦 )
50 vex ⊢ 𝑤 ∈ V
51 fnconstg ⊢ ( 𝑤 ∈ V → ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) Fn ( 𝑌 ∖ 𝑦 ) )
52 50 51 mp1i ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) Fn ( 𝑌 ∖ 𝑦 ) )
53 disjdif ⊢ ( 𝑦 ∩ ( 𝑌 ∖ 𝑦 ) ) = ∅
54 53 a1i ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑦 ∩ ( 𝑌 ∖ 𝑦 ) ) = ∅ )
55 fnun ⊢ ( ( ( 𝑧 Fn 𝑦 ∧ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) Fn ( 𝑌 ∖ 𝑦 ) ) ∧ ( 𝑦 ∩ ( 𝑌 ∖ 𝑦 ) ) = ∅ ) → ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) Fn ( 𝑦 ∪ ( 𝑌 ∖ 𝑦 ) ) )
56 49 52 54 55 syl21anc ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) Fn ( 𝑦 ∪ ( 𝑌 ∖ 𝑦 ) ) )
57 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑌 → 𝑦 ⊆ 𝑌 )
58 undif ⊢ ( 𝑦 ⊆ 𝑌 ↔ ( 𝑦 ∪ ( 𝑌 ∖ 𝑦 ) ) = 𝑌 )
59 57 58 sylib ⊢ ( 𝑦 ∈ 𝒫 𝑌 → ( 𝑦 ∪ ( 𝑌 ∖ 𝑦 ) ) = 𝑌 )
60 59 ad2antrl ⊢ ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) → ( 𝑦 ∪ ( 𝑌 ∖ 𝑦 ) ) = 𝑌 )
61 60 adantr ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑦 ∪ ( 𝑌 ∖ 𝑦 ) ) = 𝑌 )
62 61 fneq2d ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) Fn ( 𝑦 ∪ ( 𝑌 ∖ 𝑦 ) ) ↔ ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) Fn 𝑌 ) )
63 56 62 mpbid ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) Fn 𝑌 )
64 rnun ⊢ ran ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) = ( ran 𝑧 ∪ ran ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) )
65 forn ⊢ ( 𝑧 : 𝑦 –onto→ 𝑋 → ran 𝑧 = 𝑋 )
66 65 ad2antll ⊢ ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) → ran 𝑧 = 𝑋 )
67 66 adantr ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ran 𝑧 = 𝑋 )
68 67 uneq1d ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ran 𝑧 ∪ ran ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) = ( 𝑋 ∪ ran ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) )
69 fconst6g ⊢ ( 𝑤 ∈ 𝑋 → ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) : ( 𝑌 ∖ 𝑦 ) ⟶ 𝑋 )
70 69 frnd ⊢ ( 𝑤 ∈ 𝑋 → ran ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ⊆ 𝑋 )
71 70 adantl ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ran ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ⊆ 𝑋 )
72 ssequn2 ⊢ ( ran ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ⊆ 𝑋 ↔ ( 𝑋 ∪ ran ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) = 𝑋 )
73 71 72 sylib ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑋 ∪ ran ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) = 𝑋 )
74 68 73 eqtrd ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ran 𝑧 ∪ ran ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) = 𝑋 )
75 64 74 syl5eq ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ran ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) = 𝑋 )
76 df-fo ⊢ ( ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) : 𝑌 –onto→ 𝑋 ↔ ( ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) Fn 𝑌 ∧ ran ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) = 𝑋 ) )
77 63 75 76 sylanbrc ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) : 𝑌 –onto→ 𝑋 )
78 foeq1 ⊢ ( 𝑥 = ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) → ( 𝑥 : 𝑌 –onto→ 𝑋 ↔ ( 𝑧 ∪ ( ( 𝑌 ∖ 𝑦 ) × { 𝑤 } ) ) : 𝑌 –onto→ 𝑋 ) )
79 46 77 78 spcedv ⊢ ( ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 )
80 37 79 exlimddv ⊢ ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑦 ∈ 𝒫 𝑌 ∧ 𝑧 : 𝑦 –onto→ 𝑋 ) ) → ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 )
81 80 expr ⊢ ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( 𝑧 : 𝑦 –onto→ 𝑋 → ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 ) )
82 81 exlimdv ⊢ ( ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 → ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 ) )
83 82 rexlimdva ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 → ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 ) )
84 34 83 impbid ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 ↔ ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) )
85 24 84 bitrd ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 ≠ ∅ ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) )
86 22 85 pm2.61dane ⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) )
87 1 86 syl ⊢ ( 𝑌 ∈ 𝑉 → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑦 ∈ 𝒫 𝑌 ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) )