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	⊢ ( 𝜑 → 𝐴 ≼^* 𝐵 )

Metamath Proof Explorer

Theorem wdom2d

Proof