Metamath Proof Explorer

Theorem wdom2d

Description: Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep ). (Contributed by Stefan O'Rear, 13-Feb-2015)

Ref Expression
Hypotheses wdom2d.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
wdom2d.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
wdom2d.o ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑋 )
Assertion wdom2d ( 𝜑 → 𝐴 ≼* 𝐵 )

Proof

Step Hyp Ref Expression
1 wdom2d.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 wdom2d.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 wdom2d.o ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑋 )
4 rabexg ⊢ ( 𝐵 ∈ 𝑊 → { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ∈ V )
5 2 4 syl ⊢ ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ∈ V )
6 5 1 xpexd ⊢ ( 𝜑 → ( { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } × 𝐴 ) ∈ V )
7 csbeq1 ⊢ ( 𝑧 = 𝑤 → ⦋ 𝑧 / 𝑦 ⦌ 𝑋 = ⦋ 𝑤 / 𝑦 ⦌ 𝑋 )
8 7 eleq1d ⊢ ( 𝑧 = 𝑤 → ( ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ↔ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ) )
9 8 elrab ⊢ ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↔ ( 𝑤 ∈ 𝐵 ∧ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ) )
10 9 simprbi ⊢ ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } → ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ∈ 𝐴 )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ) → ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ∈ 𝐴 )
12 11 fmpttd ⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) : { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ⟶ 𝐴 )
13 fssxp ⊢ ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) : { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ⟶ 𝐴 → ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ⊆ ( { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } × 𝐴 ) )
14 12 13 syl ⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ⊆ ( { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } × 𝐴 ) )
15 6 14 ssexd ⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ∈ V )
16 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
17 16 biimpcd ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑋 → 𝑋 ∈ 𝐴 ) )
18 17 ancrd ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑋 → ( 𝑋 ∈ 𝐴 ∧ 𝑥 = 𝑋 ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = 𝑋 → ( 𝑋 ∈ 𝐴 ∧ 𝑥 = 𝑋 ) ) )
20 19 reximdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑋 → ∃ 𝑦 ∈ 𝐵 ( 𝑋 ∈ 𝐴 ∧ 𝑥 = 𝑋 ) ) )
21 3 20 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑋 ∈ 𝐴 ∧ 𝑥 = 𝑋 ) )
22 nfv ⊢ Ⅎ 𝑣 ( 𝑋 ∈ 𝐴 ∧ 𝑥 = 𝑋 )
23 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑦 ⦌ 𝑋
24 23 nfel1 ⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴
25 23 nfeq2 ⊢ Ⅎ 𝑦 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋
26 24 25 nfan ⊢ Ⅎ 𝑦 ( ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ∧ 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 )
27 csbeq1a ⊢ ( 𝑦 = 𝑣 → 𝑋 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 )
28 27 eleq1d ⊢ ( 𝑦 = 𝑣 → ( 𝑋 ∈ 𝐴 ↔ ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ) )
29 27 eqeq2d ⊢ ( 𝑦 = 𝑣 → ( 𝑥 = 𝑋 ↔ 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ) )
30 28 29 anbi12d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑋 ∈ 𝐴 ∧ 𝑥 = 𝑋 ) ↔ ( ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ∧ 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ) ) )
31 22 26 30 cbvrexw ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑋 ∈ 𝐴 ∧ 𝑥 = 𝑋 ) ↔ ∃ 𝑣 ∈ 𝐵 ( ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ∧ 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ) )
32 21 31 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑣 ∈ 𝐵 ( ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ∧ 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ) )
33 csbeq1 ⊢ ( 𝑧 = 𝑣 → ⦋ 𝑧 / 𝑦 ⦌ 𝑋 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 )
34 33 eleq1d ⊢ ( 𝑧 = 𝑣 → ( ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ↔ ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ) )
35 34 elrab ⊢ ( 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↔ ( 𝑣 ∈ 𝐵 ∧ ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ) )
36 35 simprbi ⊢ ( 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } → ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 )
37 csbeq1 ⊢ ( 𝑤 = 𝑣 → ⦋ 𝑤 / 𝑦 ⦌ 𝑋 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 )
38 eqid ⊢ ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) = ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 )
39 37 38 fvmptg ⊢ ( ( 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ∧ ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ) → ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ‘ 𝑣 ) = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 )
40 36 39 mpdan ⊢ ( 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } → ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ‘ 𝑣 ) = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 )
41 40 eqeq2d ⊢ ( 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } → ( 𝑥 = ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ‘ 𝑣 ) ↔ 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ) )
42 41 rexbiia ⊢ ( ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } 𝑥 = ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ‘ 𝑣 ) ↔ ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 )
43 34 rexrab ⊢ ( ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ↔ ∃ 𝑣 ∈ 𝐵 ( ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ∧ 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ) )
44 42 43 bitri ⊢ ( ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } 𝑥 = ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ‘ 𝑣 ) ↔ ∃ 𝑣 ∈ 𝐵 ( ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ∈ 𝐴 ∧ 𝑥 = ⦋ 𝑣 / 𝑦 ⦌ 𝑋 ) )
45 32 44 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } 𝑥 = ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ‘ 𝑣 ) )
46 45 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } 𝑥 = ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ‘ 𝑣 ) )
47 dffo3 ⊢ ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) : { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } –onto→ 𝐴 ↔ ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) : { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } 𝑥 = ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ‘ 𝑣 ) ) )
48 12 46 47 sylanbrc ⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) : { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } –onto→ 𝐴 )
49 fowdom ⊢ ( ( ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) ∈ V ∧ ( 𝑤 ∈ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑋 ) : { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } –onto→ 𝐴 ) → 𝐴 ≼* { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } )
50 15 48 49 syl2anc ⊢ ( 𝜑 → 𝐴 ≼* { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } )
51 ssrab2 ⊢ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ⊆ 𝐵
52 ssdomg ⊢ ( 𝐵 ∈ 𝑊 → ( { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ⊆ 𝐵 → { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ≼ 𝐵 ) )
53 51 52 mpi ⊢ ( 𝐵 ∈ 𝑊 → { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ≼ 𝐵 )
54 domwdom ⊢ ( { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ≼ 𝐵 → { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ≼* 𝐵 )
55 2 53 54 3syl ⊢ ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ≼* 𝐵 )
56 wdomtr ⊢ ( ( 𝐴 ≼* { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ∧ { 𝑧 ∈ 𝐵 ∣ ⦋ 𝑧 / 𝑦 ⦌ 𝑋 ∈ 𝐴 } ≼* 𝐵 ) → 𝐴 ≼* 𝐵 )
57 50 55 56 syl2anc ⊢ ( 𝜑 → 𝐴 ≼* 𝐵 )