brdom3 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem brdom3 4782

Description: Equivalence to a dominance relation.

**Hypotheses**
Ref	Expression
brdom3.1	⊢ A ∈ V
brdom3.2	⊢ B ∈ V

**Assertion**
Ref	Expression
brdom3	⊢ (A ≼ B ↔ ∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx))

Distinct variable groups: x,f,y,A B,f,x,y

**Proof of Theorem brdom3**
Step	Hyp	Ref	Expression
1		brdom3.2	. . . . . . 7 ⊢ B ∈ V
2		fodomr 4470	. . . . . . 7 ⊢ ((B ∈ V ⋀ ∅ ≺ A ⋀ A ≼ B) → ∃f f:B–onto→A)
3	1, 2	mp3an1 901	. . . . . 6 ⊢ ((∅ ≺ A ⋀ A ≼ B) → ∃f f:B–onto→A)
4		brdom3.1	. . . . . . . 8 ⊢ A ∈ V
5	4	0sdom 4454	. . . . . . 7 ⊢ (∅ ≺ A ↔ A ≠ ∅)
6		df-ne 1584	. . . . . . 7 ⊢ (A ≠ ∅ ↔ ¬ A = ∅)
7	5, 6	bitr2 174	. . . . . 6 ⊢ (¬ A = ∅ ↔ ∅ ≺ A)
8	3, 7	sylanb 449	. . . . 5 ⊢ ((¬ A = ∅ ⋀ A ≼ B) → ∃f f:B–onto→A)
9	8	ancoms 436	. . . 4 ⊢ ((A ≼ B ⋀ ¬ A = ∅) → ∃f f:B–onto→A)
10		pm5.6 687	. . . 4 ⊢ (((A ≼ B ⋀ ¬ A = ∅) → ∃f f:B–onto→A) ↔ (A ≼ B → (A = ∅ ⋁ ∃f f:B–onto→A)))
11	9, 10	mpbi 189	. . 3 ⊢ (A ≼ B → (A = ∅ ⋁ ∃f f:B–onto→A))
12		rzal 2351	. . . . . 6 ⊢ (A = ∅ → ∀x ∈ A ∃y ∈ B y∅x)
13		noel 2280	. . . . . . . . . 10 ⊢ ¬ ⟨x, y⟩ ∈ ∅
14		df-br 2615	. . . . . . . . . 10 ⊢ (x∅y ↔ ⟨x, y⟩ ∈ ∅)
15	13, 14	mtbir 192	. . . . . . . . 9 ⊢ ¬ x∅y
16	15	nex 1099	. . . . . . . 8 ⊢ ¬ ∃y x∅y
17		exmo 1414	. . . . . . . . 9 ⊢ (∃y x∅y ⋁ ∃*y x∅y)
18	17	ori 230	. . . . . . . 8 ⊢ (¬ ∃y x∅y → ∃*y x∅y)
19	16, 18	ax-mp 7	. . . . . . 7 ⊢ ∃*y x∅y
20	19	ax-gen 961	. . . . . 6 ⊢ ∀x∃*y x∅y
21	12, 20	jctil 292	. . . . 5 ⊢ (A = ∅ → (∀x∃*y x∅y ⋀ ∀x ∈ A ∃y ∈ B y∅x))
22		0ex 2706	. . . . . 6 ⊢ ∅ ∈ V
23		ax-17 969	. . . . . . . . 9 ⊢ (f = ∅ → ∀y f = ∅)
24		breq 2616	. . . . . . . . 9 ⊢ (f = ∅ → (xfy ↔ x∅y))
25	23, 24	mobid 1402	. . . . . . . 8 ⊢ (f = ∅ → (∃y xfy ↔ ∃y x∅y))
26	25	albidv 1276	. . . . . . 7 ⊢ (f = ∅ → (∀x∃y xfy ↔ ∀x∃y x∅y))
27		breq 2616	. . . . . . . . 9 ⊢ (f = ∅ → (yfx ↔ y∅x))
28	27	rexbidv 1661	. . . . . . . 8 ⊢ (f = ∅ → (∃y ∈ B yfx ↔ ∃y ∈ B y∅x))
29	28	ralbidv 1660	. . . . . . 7 ⊢ (f = ∅ → (∀x ∈ A ∃y ∈ B yfx ↔ ∀x ∈ A ∃y ∈ B y∅x))
30	26, 29	anbi12d 627	. . . . . 6 ⊢ (f = ∅ → ((∀x∃y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx) ↔ (∀x∃y x∅y ⋀ ∀x ∈ A ∃y ∈ B y∅x)))
31	22, 30	cla4ev 1865	. . . . 5 ⊢ ((∀x∃y x∅y ⋀ ∀x ∈ A ∃y ∈ B y∅x) → ∃f(∀x∃y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx))
32	21, 31	syl 10	. . . 4 ⊢ (A = ∅ → ∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx))
33		fofun 3665	. . . . . . 7 ⊢ (f:B–onto→A → Fun f)
34		dffunmo 3524	. . . . . . . 8 ⊢ (Fun f ↔ (Rel f ⋀ ∀x∃*y xfy))
35	34	pm3.27bi 326	. . . . . . 7 ⊢ (Fun f → ∀x∃*y xfy)
36	33, 35	syl 10	. . . . . 6 ⊢ (f:B–onto→A → ∀x∃*y xfy)
37		dffo4 3812	. . . . . . 7 ⊢ (f:B–onto→A ↔ (f:B–→A ⋀ ∀x ∈ A ∃y ∈ B yfx))
38	37	pm3.27bi 326	. . . . . 6 ⊢ (f:B–onto→A → ∀x ∈ A ∃y ∈ B yfx)
39	36, 38	jca 288	. . . . 5 ⊢ (f:B–onto→A → (∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx))
40	39	19.22i 1038	. . . 4 ⊢ (∃f f:B–onto→A → ∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx))
41	32, 40	jaoi 341	. . 3 ⊢ ((A = ∅ ⋁ ∃f f:B–onto→A) → ∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx))
42	11, 41	syl 10	. 2 ⊢ (A ≼ B → ∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx))
43		inss1 2226	. . . . . . . . . . 11 ⊢ (f ∩ (B × A)) ⊆ f
44	43	ssbri 2652	. . . . . . . . . 10 ⊢ (x(f ∩ (B × A))y → xfy)
45	44	immoi 1416	. . . . . . . . 9 ⊢ (∃y xfy → ∃y x(f ∩ (B × A))y)
46	45	19.20i 990	. . . . . . . 8 ⊢ (∀x∃y xfy → ∀x∃y x(f ∩ (B × A))y)
47		dffunmo 3524	. . . . . . . . 9 ⊢ (Fun (f ∩ (B × A)) ↔ (Rel (f ∩ (B × A)) ⋀ ∀x∃*y x(f ∩ (B × A))y))
48		relxp 3250	. . . . . . . . . 10 ⊢ Rel (B × A)
49		relin2 3258	. . . . . . . . . 10 ⊢ (Rel (B × A) → Rel (f ∩ (B × A)))
50	48, 49	ax-mp 7	. . . . . . . . 9 ⊢ Rel (f ∩ (B × A))
51	47, 50	mpbiran 727	. . . . . . . 8 ⊢ (Fun (f ∩ (B × A)) ↔ ∀x∃*y x(f ∩ (B × A))y)
52	46, 51	sylibr 200	. . . . . . 7 ⊢ (∀x∃*y xfy → Fun (f ∩ (B × A)))
53		funfn 3535	. . . . . . 7 ⊢ (Fun (f ∩ (B × A)) ↔ (f ∩ (B × A)) Fn dom ( f ∩ (B × A)))
54	52, 53	sylib 198	. . . . . 6 ⊢ (∀x∃*y xfy → (f ∩ (B × A)) Fn dom ( f ∩ (B × A)))
55		rninxp 3475	. . . . . . 7 ⊢ (ran ( f ∩ (B × A)) = A ↔ ∀x ∈ A ∃y ∈ B yfx)
56	55	biimpr 152	. . . . . 6 ⊢ (∀x ∈ A ∃y ∈ B yfx → ran ( f ∩ (B × A)) = A)
57	54, 56	anim12i 333	. . . . 5 ⊢ ((∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx) → ((f ∩ (B × A)) Fn dom ( f ∩ (B × A)) ⋀ ran ( f ∩ (B × A)) = A))
58		df-fo 3191	. . . . 5 ⊢ ((f ∩ (B × A)):dom ( f ∩ (B × A))–onto→A ↔ ((f ∩ (B × A)) Fn dom ( f ∩ (B × A)) ⋀ ran ( f ∩ (B × A)) = A))
59	57, 58	sylibr 200	. . . 4 ⊢ ((∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx) → (f ∩ (B × A)):dom ( f ∩ (B × A))–onto→A)
60		visset 1809	. . . . . . 7 ⊢ f ∈ V
61	60	inex1 2711	. . . . . 6 ⊢ (f ∩ (B × A)) ∈ V
62	61	dmex 3354	. . . . 5 ⊢ dom ( f ∩ (B × A)) ∈ V
63	62	fodom 4779	. . . 4 ⊢ ((f ∩ (B × A)):dom ( f ∩ (B × A))–onto→A → A ≼ dom ( f ∩ (B × A)))
64		inss2 2227	. . . . . . . 8 ⊢ (f ∩ (B × A)) ⊆ (B × A)
65		dmss 3305	. . . . . . . 8 ⊢ ((f ∩ (B × A)) ⊆ (B × A) → dom ( f ∩ (B × A)) ⊆ dom ( B × A))
66	64, 65	ax-mp 7	. . . . . . 7 ⊢ dom ( f ∩ (B × A)) ⊆ dom ( B × A)
67		dmxpss 3466	. . . . . . 7 ⊢ dom ( B × A) ⊆ B
68	66, 67	sstri 2069	. . . . . 6 ⊢ dom ( f ∩ (B × A)) ⊆ B
69		ssdom2g 4397	. . . . . 6 ⊢ (B ∈ V → (dom ( f ∩ (B × A)) ⊆ B → dom ( f ∩ (B × A)) ≼ B))
70	1, 68, 69	mp2 43	. . . . 5 ⊢ dom ( f ∩ (B × A)) ≼ B
71		domtr 4403	. . . . 5 ⊢ ((A ≼ dom ( f ∩ (B × A)) ⋀ dom ( f ∩ (B × A)) ≼ B) → A ≼ B)
72	70, 71	mpan2 695	. . . 4 ⊢ (A ≼ dom ( f ∩ (B × A)) → A ≼ B)
73	59, 63, 72	3syl 20	. . 3 ⊢ ((∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx) → A ≼ B)
74	73	19.23aiv 1293	. 2 ⊢ (∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx) → A ≼ B)
75	42, 74	impbi 157	1 ⊢ (A ≼ B ↔ ∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx))

Colors of variables: wff set class

Syntax hints: ¬ wn 2 → wi 3 ↔ wb 146 ⋁ wo 222 ⋀ wa 223 ∀wal 952 = wceq 954 ∈ wcel 956 ∃wex 978 ∃*wmo 1379 ≠ wne 1582 ∀wral 1642 ∃wrex 1643 Vcvv 1807 ∩ cin 2042 ⊆ wss 2043 ∅c0 2276 ⟨cop 2407 class class class wbr 2614 × cxp 3163 dom cdm 3165 ran crn 3166 Rel wrel 3170 Fun wfun 3171 Fn wfn 3172 –→wf 3173 –onto→wfo 3175 ≼ cdom 4356 ≺ csdm 4357

This theorem is referenced by: brdom5 4783 brdom4 4784

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861 ax-ac 4725

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-nul 2277 df-pw 2398 df-sn 2408 df-pr 2409 df-op 2412 df-uni 2499 df-br 2615 df-opab 2662 df-id 2830 df-xp 3179 df-rel 3180 df-cnv 3181 df-co 3182 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fun 3187 df-fn 3188 df-f 3189 df-f1 3190 df-fo 3191 df-f1o 3192 df-fv 3193 df-er 4252 df-en 4358 df-dom 4359 df-sdom 4360