Theorem brdom4 4784

Description: An equivalence to a dominance relation.

Hypotheses

Ref	Expression
brdom4.1	⊢ A ∈ V
brdom4.2	⊢ B ∈ V

Assertion

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

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

Proof of Theorem brdom4

Step	Hyp	Ref	Expression
1		brdom4.1	. . . 4 ⊢ A ∈ V
2		brdom4.2	. . . 4 ⊢ B ∈ V
3	1, 2	brdom3 4782	. . 3 ⊢ (A ≼ B ↔ ∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx))
4		moan 1420	. . . . . . 7 ⊢ (∃*y xfy → ∃*y(y ∈ A ⋀ xfy))
5	4	19.20i 990	. . . . . 6 ⊢ (∀x∃*y xfy → ∀x∃*y(y ∈ A ⋀ xfy))
6		alral 1689	. . . . . 6 ⊢ (∀x∃*y(y ∈ A ⋀ xfy) → ∀x ∈ B ∃*y(y ∈ A ⋀ xfy))
7	5, 6	syl 10	. . . . 5 ⊢ (∀x∃*y xfy → ∀x ∈ B ∃*y(y ∈ A ⋀ xfy))
8	7	anim1i 334	. . . 4 ⊢ ((∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx) → (∀x ∈ B ∃*y(y ∈ A ⋀ xfy) ⋀ ∀x ∈ A ∃y ∈ B yfx))
9	8	19.22i 1038	. . 3 ⊢ (∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx) → ∃f(∀x ∈ B ∃*y(y ∈ A ⋀ xfy) ⋀ ∀x ∈ A ∃y ∈ B yfx))
10	3, 9	sylbi 199	. 2 ⊢ (A ≼ B → ∃f(∀x ∈ B ∃*y(y ∈ A ⋀ xfy) ⋀ ∀x ∈ A ∃y ∈ B yfx))
11		inss2 2227	. . . . . . . . . . . . . 14 ⊢ (f ∩ (B × A)) ⊆ (B × A)
12		dmss 3305	. . . . . . . . . . . . . 14 ⊢ ((f ∩ (B × A)) ⊆ (B × A) → dom ( f ∩ (B × A)) ⊆ dom ( B × A))
13	11, 12	ax-mp 7	. . . . . . . . . . . . 13 ⊢ dom ( f ∩ (B × A)) ⊆ dom ( B × A)
14		dmxpss 3466	. . . . . . . . . . . . 13 ⊢ dom ( B × A) ⊆ B
15	13, 14	sstri 2069	. . . . . . . . . . . 12 ⊢ dom ( f ∩ (B × A)) ⊆ B
16	15	sseli 2061	. . . . . . . . . . 11 ⊢ (x ∈ dom ( f ∩ (B × A)) → x ∈ B)
17		rnss 3337	. . . . . . . . . . . . . . . 16 ⊢ ((f ∩ (B × A)) ⊆ (B × A) → ran ( f ∩ (B × A)) ⊆ ran ( B × A))
18	11, 17	ax-mp 7	. . . . . . . . . . . . . . 15 ⊢ ran ( f ∩ (B × A)) ⊆ ran ( B × A)
19		rnxpss 3467	. . . . . . . . . . . . . . 15 ⊢ ran ( B × A) ⊆ A
20	18, 19	sstri 2069	. . . . . . . . . . . . . 14 ⊢ ran ( f ∩ (B × A)) ⊆ A
21	20	sseli 2061	. . . . . . . . . . . . 13 ⊢ (y ∈ ran ( f ∩ (B × A)) → y ∈ A)
22		inss1 2226	. . . . . . . . . . . . . 14 ⊢ (f ∩ (B × A)) ⊆ f
23	22	ssbri 2652	. . . . . . . . . . . . 13 ⊢ (x(f ∩ (B × A))y → xfy)
24	21, 23	anim12i 333	. . . . . . . . . . . 12 ⊢ ((y ∈ ran ( f ∩ (B × A)) ⋀ x(f ∩ (B × A))y) → (y ∈ A ⋀ xfy))
25	24	immoi 1416	. . . . . . . . . . 11 ⊢ (∃*y(y ∈ A ⋀ xfy) → ∃*y(y ∈ ran ( f ∩ (B × A)) ⋀ x(f ∩ (B × A))y))
26	16, 25	imim12i 18	. . . . . . . . . 10 ⊢ ((x ∈ B → ∃*y(y ∈ A ⋀ xfy)) → (x ∈ dom ( f ∩ (B × A)) → ∃*y(y ∈ ran ( f ∩ (B × A)) ⋀ x(f ∩ (B × A))y)))
27	26	r19.20i2 1700	. . . . . . . . 9 ⊢ (∀x ∈ B ∃*y(y ∈ A ⋀ xfy) → ∀x ∈ dom ( f ∩ (B × A))∃*y(y ∈ ran ( f ∩ (B × A)) ⋀ x(f ∩ (B × A))y))
28		relxp 3250	. . . . . . . . . 10 ⊢ Rel (B × A)
29		relin2 3258	. . . . . . . . . 10 ⊢ (Rel (B × A) → Rel (f ∩ (B × A)))
30	28, 29	ax-mp 7	. . . . . . . . 9 ⊢ Rel (f ∩ (B × A))
31	27, 30	jctil 292	. . . . . . . 8 ⊢ (∀x ∈ B ∃*y(y ∈ A ⋀ xfy) → (Rel (f ∩ (B × A)) ⋀ ∀x ∈ dom ( f ∩ (B × A))∃*y(y ∈ ran ( f ∩ (B × A)) ⋀ x(f ∩ (B × A))y)))
32		dffun8 3534	. . . . . . . 8 ⊢ (Fun (f ∩ (B × A)) ↔ (Rel (f ∩ (B × A)) ⋀ ∀x ∈ dom ( f ∩ (B × A))∃*y(y ∈ ran ( f ∩ (B × A)) ⋀ x(f ∩ (B × A))y)))
33	31, 32	sylibr 200	. . . . . . 7 ⊢ (∀x ∈ B ∃*y(y ∈ A ⋀ xfy) → Fun (f ∩ (B × A)))
34		funfn 3535	. . . . . . 7 ⊢ (Fun (f ∩ (B × A)) ↔ (f ∩ (B × A)) Fn dom ( f ∩ (B × A)))
35	33, 34	sylib 198	. . . . . 6 ⊢ (∀x ∈ B ∃*y(y ∈ A ⋀ xfy) → (f ∩ (B × A)) Fn dom ( f ∩ (B × A)))
36		rninxp 3475	. . . . . . 7 ⊢ (ran ( f ∩ (B × A)) = A ↔ ∀x ∈ A ∃y ∈ B yfx)
37	36	biimpr 152	. . . . . 6 ⊢ (∀x ∈ A ∃y ∈ B yfx → ran ( f ∩ (B × A)) = A)
38	35, 37	anim12i 333	. . . . 5 ⊢ ((∀x ∈ B ∃*y(y ∈ A ⋀ xfy) ⋀ ∀x ∈ A ∃y ∈ B yfx) → ((f ∩ (B × A)) Fn dom ( f ∩ (B × A)) ⋀ ran ( f ∩ (B × A)) = A))
39		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))
40	38, 39	sylibr 200	. . . 4 ⊢ ((∀x ∈ B ∃*y(y ∈ A ⋀ xfy) ⋀ ∀x ∈ A ∃y ∈ B yfx) → (f ∩ (B × A)):dom ( f ∩ (B × A))–onto→A)
41		visset 1809	. . . . . . 7 ⊢ f ∈ V
42	41	inex1 2711	. . . . . 6 ⊢ (f ∩ (B × A)) ∈ V
43	42	dmex 3354	. . . . 5 ⊢ dom ( f ∩ (B × A)) ∈ V
44	43	fodom 4779	. . . 4 ⊢ ((f ∩ (B × A)):dom ( f ∩ (B × A))–onto→A → A ≼ dom ( f ∩ (B × A)))
45		ssdom2g 4397	. . . . . 6 ⊢ (B ∈ V → (dom ( f ∩ (B × A)) ⊆ B → dom ( f ∩ (B × A)) ≼ B))
46	2, 15, 45	mp2 43	. . . . 5 ⊢ dom ( f ∩ (B × A)) ≼ B
47		domtr 4403	. . . . 5 ⊢ ((A ≼ dom ( f ∩ (B × A)) ⋀ dom ( f ∩ (B × A)) ≼ B) → A ≼ B)
48	46, 47	mpan2 695	. . . 4 ⊢ (A ≼ dom ( f ∩ (B × A)) → A ≼ B)
49	40, 44, 48	3syl 20	. . 3 ⊢ ((∀x ∈ B ∃*y(y ∈ A ⋀ xfy) ⋀ ∀x ∈ A ∃y ∈ B yfx) → A ≼ B)
50	49	19.23aiv 1293	. 2 ⊢ (∃f(∀x ∈ B ∃*y(y ∈ A ⋀ xfy) ⋀ ∀x ∈ A ∃y ∈ B yfx) → A ≼ B)
51	10, 50	impbi 157	1 ⊢ (A ≼ B ↔ ∃f(∀x ∈ B ∃*y(y ∈ A ⋀ xfy) ⋀ ∀x ∈ A ∃y ∈ B yfx))

Syntax hints:   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  ∃*wmo 1379  ∀wral 1642  ∃wrex 1643  Vcvv 1807   ∩ cin 2042   ⊆ wss 2043   class class class wbr 2614   × cxp 3163  dom cdm 3165  ran crn 3166  Rel wrel 3170  Fun wfun 3171   Fn wfn 3172  –onto→wfo 3175   ≼ cdom 4356

This theorem is referenced by:  brdom7disj 4785

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

Copyright terms: Public domain