Theorem brdom5 9634

Description: An equivalence to a dominance relation. (Contributed by NM, 29-Mar-2007.)

Hypothesis

Ref	Expression
brdom3.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
brdom5	⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥))

Distinct variable groups:   𝑥,𝑓,𝑦,𝐴   𝐵,𝑓,𝑥,𝑦

Proof of Theorem brdom5

Step	Hyp	Ref	Expression
1		brdom3.2	. . . 4 ⊢ 𝐵 ∈ V
2	1	brdom3 9633	. . 3 ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥))
3		alral 3114	. . . . 5 ⊢ (∀𝑥∃*𝑦 𝑥𝑓𝑦 → ∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦)
4	3	anim1i 604	. . . 4 ⊢ ((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥))
5	4	eximi 1919	. . 3 ⊢ (∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥))
6	2, 5	sylbi 208	. 2 ⊢ (𝐴 ≼ 𝐵 → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥))
7		inss2 4028	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴)
8		dmss 5522	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) → dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴))
9	7, 8	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴)
10		dmxpss 5774	. . . . . . . . . . . . 13 ⊢ dom (𝐵 × 𝐴) ⊆ 𝐵
11	9, 10	sstri 3805	. . . . . . . . . . . 12 ⊢ dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵
12	11	sseli 3792	. . . . . . . . . . 11 ⊢ (𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴)) → 𝑥 ∈ 𝐵)
13		inss1 4027	. . . . . . . . . . . . 13 ⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝑓
14	13	ssbri 4887	. . . . . . . . . . . 12 ⊢ (𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦 → 𝑥𝑓𝑦)
15	14	moimi 2681	. . . . . . . . . . 11 ⊢ (∃*𝑦 𝑥𝑓𝑦 → ∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)
16	12, 15	imim12i 62	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 → ∃*𝑦 𝑥𝑓𝑦) → (𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴)) → ∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦))
17	16	ralimi2 3135	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 → ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)
18		relxp 5326	. . . . . . . . . 10 ⊢ Rel (𝐵 × 𝐴)
19		relin2 5436	. . . . . . . . . 10 ⊢ (Rel (𝐵 × 𝐴) → Rel (𝑓 ∩ (𝐵 × 𝐴)))
20	18, 19	ax-mp 5	. . . . . . . . 9 ⊢ Rel (𝑓 ∩ (𝐵 × 𝐴))
21	17, 20	jctil 511	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 → (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦))
22		dffun7 6126	. . . . . . . 8 ⊢ (Fun (𝑓 ∩ (𝐵 × 𝐴)) ↔ (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦))
23	21, 22	sylibr 225	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 → Fun (𝑓 ∩ (𝐵 × 𝐴)))
24		funfn 6129	. . . . . . 7 ⊢ (Fun (𝑓 ∩ (𝐵 × 𝐴)) ↔ (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)))
25	23, 24	sylib 209	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 → (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)))
26		rninxp 5782	. . . . . . 7 ⊢ (ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)
27	26	biimpri 219	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 → ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)
28	25, 27	anim12i 602	. . . . 5 ⊢ ((∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴))
29		df-fo 6105	. . . . 5 ⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 ↔ ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴))
30	28, 29	sylibr 225	. . . 4 ⊢ ((∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴)
31		vex 3392	. . . . . . 7 ⊢ 𝑓 ∈ V
32	31	inex1 4992	. . . . . 6 ⊢ (𝑓 ∩ (𝐵 × 𝐴)) ∈ V
33	32	dmex 7327	. . . . 5 ⊢ dom (𝑓 ∩ (𝐵 × 𝐴)) ∈ V
34	33	fodom 9627	. . . 4 ⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 → 𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)))
35		ssdomg 8236	. . . . . 6 ⊢ (𝐵 ∈ V → (dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 → dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵))
36	1, 11, 35	mp2 9	. . . . 5 ⊢ dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵
37		domtr 8243	. . . . 5 ⊢ ((𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵) → 𝐴 ≼ 𝐵)
38	36, 37	mpan2 674	. . . 4 ⊢ (𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) → 𝐴 ≼ 𝐵)
39	30, 34, 38	3syl 18	. . 3 ⊢ ((∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵)
40	39	exlimiv 2021	. 2 ⊢ (∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵)
41	6, 40	impbii 200	1 ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥))

Syntax hints:   ↔ wb 197   ∧ wa 384  ∀wal 1635   = wceq 1637  ∃wex 1859   ∈ wcel 2156  ∃*wmo 2631  ∀wral 3094  ∃wrex 3095  Vcvv 3389   ∩ cin 3766   ⊆ wss 3767   class class class wbr 4842   × cxp 5307  dom cdm 5309  ran crn 5310  Rel wrel 5314  Fun wfun 6093   Fn wfn 6094  –onto→wfo 6097   ≼ cdom 8188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5094  ax-un 7177  ax-ac2 9568

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-ral 3099  df-rex 3100  df-reu 3101  df-rmo 3102  df-rab 3103  df-v 3391  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4115  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-tp 4373  df-op 4375  df-uni 4629  df-int 4668  df-iun 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5217  df-eprel 5222  df-po 5230  df-so 5231  df-fr 5268  df-se 5269  df-we 5270  df-xp 5315  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-res 5321  df-ima 5322  df-pred 5891  df-ord 5937  df-on 5938  df-suc 5940  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-isom 6108  df-riota 6833  df-ov 6875  df-oprab 6876  df-mpt2 6877  df-1st 7396  df-2nd 7397  df-wrecs 7640  df-recs 7702  df-er 7977  df-map 8092  df-en 8191  df-dom 8192  df-sdom 8193  df-card 9046  df-acn 9049  df-ac 9220

This theorem is referenced by:  brdom6disj  9637