Theorem brdom3

Description: Equivalence to a dominance relation. (Contributed by NM, 27-Mar-2007)

	Ref	Expression
Hypothesis	brdom3.2	⊢ 𝐵 ∈ V
Assertion	brdom3	⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		brdom3.2	⊢ 𝐵 ∈ V
2		reldom	⊢ Rel ≼
3	2	brrelex1i	⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V )
4		0sdomg	⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
5	3 4	syl	⊢ ( 𝐴 ≼ 𝐵 → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
6		df-ne	⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
7	5 6	bitrdi	⊢ ( 𝐴 ≼ 𝐵 → ( ∅ ≺ 𝐴 ↔ ¬ 𝐴 = ∅ ) )
8	7	biimpar	⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅ ) → ∅ ≺ 𝐴 )
9		fodomr	⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 )
10	9	ancoms	⊢ ( ( 𝐴 ≼ 𝐵 ∧ ∅ ≺ 𝐴 ) → ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 )
11	8 10	syldan	⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 )
12		pm5.6	⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 ) ↔ ( 𝐴 ≼ 𝐵 → ( 𝐴 = ∅ ∨ ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 ) ) )
13	11 12	mpbi	⊢ ( 𝐴 ≼ 𝐵 → ( 𝐴 = ∅ ∨ ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 ) )
14		br0	⊢ ¬ 𝑥 ∅ 𝑦
15	14	nex	⊢ ¬ ∃ 𝑦 𝑥 ∅ 𝑦
16		exmo	⊢ ( ∃ 𝑦 𝑥 ∅ 𝑦 ∨ ∃* 𝑦 𝑥 ∅ 𝑦 )
17	15 16	mtpor	⊢ ∃* 𝑦 𝑥 ∅ 𝑦
18	17	ax-gen	⊢ ∀ 𝑥 ∃* 𝑦 𝑥 ∅ 𝑦
19		rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 ∅ 𝑥 )
20		0ex	⊢ ∅ ∈ V
21		breq	⊢ ( 𝑓 = ∅ → ( 𝑥 𝑓 𝑦 ↔ 𝑥 ∅ 𝑦 ) )
22	21	mobidv	⊢ ( 𝑓 = ∅ → ( ∃* 𝑦 𝑥 𝑓 𝑦 ↔ ∃* 𝑦 𝑥 ∅ 𝑦 ) )
23	22	albidv	⊢ ( 𝑓 = ∅ → ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ↔ ∀ 𝑥 ∃* 𝑦 𝑥 ∅ 𝑦 ) )
24		breq	⊢ ( 𝑓 = ∅ → ( 𝑦 𝑓 𝑥 ↔ 𝑦 ∅ 𝑥 ) )
25	24	rexbidv	⊢ ( 𝑓 = ∅ → ( ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑦 ∅ 𝑥 ) )
26	25	ralbidv	⊢ ( 𝑓 = ∅ → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 ∅ 𝑥 ) )
27	23 26	anbi12d	⊢ ( 𝑓 = ∅ → ( ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) ↔ ( ∀ 𝑥 ∃* 𝑦 𝑥 ∅ 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 ∅ 𝑥 ) ) )
28	20 27	spcev	⊢ ( ( ∀ 𝑥 ∃* 𝑦 𝑥 ∅ 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 ∅ 𝑥 ) → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )
29	18 19 28	sylancr	⊢ ( 𝐴 = ∅ → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )
30		fofun	⊢ ( 𝑓 : 𝐵 –onto→ 𝐴 → Fun 𝑓 )
31		dffun6	⊢ ( Fun 𝑓 ↔ ( Rel 𝑓 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ) )
32	31	simprbi	⊢ ( Fun 𝑓 → ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 )
33	30 32	syl	⊢ ( 𝑓 : 𝐵 –onto→ 𝐴 → ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 )
34		dffo4	⊢ ( 𝑓 : 𝐵 –onto→ 𝐴 ↔ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )
35	34	simprbi	⊢ ( 𝑓 : 𝐵 –onto→ 𝐴 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 )
36	33 35	jca	⊢ ( 𝑓 : 𝐵 –onto→ 𝐴 → ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )
37	36	eximi	⊢ ( ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )
38	29 37	jaoi	⊢ ( ( 𝐴 = ∅ ∨ ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 ) → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )
39	13 38	syl	⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )
40		inss1	⊢ ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝑓
41	40	ssbri	⊢ ( 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 → 𝑥 𝑓 𝑦 )
42	41	moimi	⊢ ( ∃* 𝑦 𝑥 𝑓 𝑦 → ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 )
43	42	alimi	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 → ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 )
44		relinxp	⊢ Rel ( 𝑓 ∩ ( 𝐵 × 𝐴 ) )
45		dffun6	⊢ ( Fun ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ↔ ( Rel ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 ) )
46	44 45	mpbiran	⊢ ( Fun ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ↔ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) 𝑦 )
47	43 46	sylibr	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 → Fun ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) )
48	47	funfnd	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 → ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) Fn dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) )
49		rninxp	⊢ ( ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 )
50	49	biimpri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 → ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 )
51	48 50	anim12i	⊢ ( ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) Fn dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ) )
52		df-fo	⊢ ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) : dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) –onto→ 𝐴 ↔ ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) Fn dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ ran ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ) )
53	51 52	sylibr	⊢ ( ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) : dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) –onto→ 𝐴 )
54		vex	⊢ 𝑓 ∈ V
55	54	inex1	⊢ ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∈ V
56	55	dmex	⊢ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∈ V
57	56	fodom	⊢ ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) : dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) –onto→ 𝐴 → 𝐴 ≼ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) )
58		inss2	⊢ ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ ( 𝐵 × 𝐴 )
59		dmss	⊢ ( ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ ( 𝐵 × 𝐴 ) → dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ dom ( 𝐵 × 𝐴 ) )
60	58 59	ax-mp	⊢ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ dom ( 𝐵 × 𝐴 )
61		dmxpss	⊢ dom ( 𝐵 × 𝐴 ) ⊆ 𝐵
62	60 61	sstri	⊢ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝐵
63		ssdomg	⊢ ( 𝐵 ∈ V → ( dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝐵 → dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ≼ 𝐵 ) )
64	1 62 63	mp2	⊢ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ≼ 𝐵
65		domtr	⊢ ( ( 𝐴 ≼ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ∧ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) ≼ 𝐵 ) → 𝐴 ≼ 𝐵 )
66	64 65	mpan2	⊢ ( 𝐴 ≼ dom ( 𝑓 ∩ ( 𝐵 × 𝐴 ) ) → 𝐴 ≼ 𝐵 )
67	53 57 66	3syl	⊢ ( ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → 𝐴 ≼ 𝐵 )
68	67	exlimiv	⊢ ( ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) → 𝐴 ≼ 𝐵 )
69	39 68	impbii	⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∃* 𝑦 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑓 𝑥 ) )