Theorem dfac8clem 9940

Description: Lemma for dfac8c 9941. (Contributed by Mario Carneiro, 10-Jan-2013.)

Hypothesis

Ref	Expression
dfac8clem.1	⊢ 𝐹 = (𝑠 ∈ (𝐴 ∖ {∅}) ↦ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎))

Assertion

Ref	Expression
dfac8clem	⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))

Distinct variable groups:   𝑎,𝑏,𝑓,𝑟,𝑠,𝑧,𝐴   𝐵,𝑟,𝑠   𝑓,𝐹,𝑧

Allowed substitution hints:   𝐵(𝑧,𝑓,𝑎,𝑏)   𝐹(𝑠,𝑟,𝑎,𝑏)

Proof of Theorem dfac8clem

Step	Hyp	Ref	Expression
1		eldifsn 4740	. . . . . . 7 ⊢ (𝑠 ∈ (𝐴 ∖ {∅}) ↔ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅))
2		elssuni 4892	. . . . . . . . 9 ⊢ (𝑠 ∈ 𝐴 → 𝑠 ⊆ ∪ 𝐴)
3	2	ad2antrl 728	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅)) → 𝑠 ⊆ ∪ 𝐴)
4		simplr 768	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅)) → 𝑟 We ∪ 𝐴)
5		vex 3442	. . . . . . . . . . 11 ⊢ 𝑟 ∈ V
6		exse2 7857	. . . . . . . . . . 11 ⊢ (𝑟 ∈ V → 𝑟 Se ∪ 𝐴)
7	5, 6	mp1i 13	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅)) → 𝑟 Se ∪ 𝐴)
8		simprr 772	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
9		wereu2 5619	. . . . . . . . . 10 ⊢ (((𝑟 We ∪ 𝐴 ∧ 𝑟 Se ∪ 𝐴) ∧ (𝑠 ⊆ ∪ 𝐴 ∧ 𝑠 ≠ ∅)) → ∃!𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎)
10	4, 7, 3, 8, 9	syl22anc 838	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅)) → ∃!𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎)
11		riotacl 7330	. . . . . . . . 9 ⊢ (∃!𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎 → (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎) ∈ 𝑠)
12	10, 11	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅)) → (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎) ∈ 𝑠)
13	3, 12	sseldd 3932	. . . . . . 7 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅)) → (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎) ∈ ∪ 𝐴)
14	1, 13	sylan2b 594	. . . . . 6 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ 𝑠 ∈ (𝐴 ∖ {∅})) → (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎) ∈ ∪ 𝐴)
15		dfac8clem.1	. . . . . 6 ⊢ 𝐹 = (𝑠 ∈ (𝐴 ∖ {∅}) ↦ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎))
16	14, 15	fmptd 7057	. . . . 5 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) → 𝐹:(𝐴 ∖ {∅})⟶∪ 𝐴)
17		difexg 5272	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∖ {∅}) ∈ V)
18	17	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) → (𝐴 ∖ {∅}) ∈ V)
19		uniexg 7683	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ∪ 𝐴 ∈ V)
20	19	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) → ∪ 𝐴 ∈ V)
21		fex2 7876	. . . . 5 ⊢ ((𝐹:(𝐴 ∖ {∅})⟶∪ 𝐴 ∧ (𝐴 ∖ {∅}) ∈ V ∧ ∪ 𝐴 ∈ V) → 𝐹 ∈ V)
22	16, 18, 20, 21	syl3anc 1373	. . . 4 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) → 𝐹 ∈ V)
23		riotaex 7317	. . . . . . . . . . 11 ⊢ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎) ∈ V
24	15	fvmpt2 6950	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ (𝐴 ∖ {∅}) ∧ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎) ∈ V) → (𝐹‘𝑠) = (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎))
25	23, 24	mpan2 691	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴 ∖ {∅}) → (𝐹‘𝑠) = (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎))
26	1, 25	sylbir 235	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅) → (𝐹‘𝑠) = (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎))
27	26	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅)) → (𝐹‘𝑠) = (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎))
28	27, 12	eqeltrd 2834	. . . . . . 7 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅)) → (𝐹‘𝑠) ∈ 𝑠)
29	28	expr 456	. . . . . 6 ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝑠 ≠ ∅ → (𝐹‘𝑠) ∈ 𝑠))
30	29	ralrimiva 3126	. . . . 5 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑠 ≠ ∅ → (𝐹‘𝑠) ∈ 𝑠))
31		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑠 𝑧 ≠ ∅
32		nfmpt1 5195	. . . . . . . . . 10 ⊢ Ⅎ𝑠(𝑠 ∈ (𝐴 ∖ {∅}) ↦ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎))
33	15, 32	nfcxfr 2894	. . . . . . . . 9 ⊢ Ⅎ𝑠𝐹
34		nfcv 2896	. . . . . . . . 9 ⊢ Ⅎ𝑠𝑧
35	33, 34	nffv 6842	. . . . . . . 8 ⊢ Ⅎ𝑠(𝐹‘𝑧)
36	35	nfel1 2913	. . . . . . 7 ⊢ Ⅎ𝑠(𝐹‘𝑧) ∈ 𝑧
37	31, 36	nfim 1897	. . . . . 6 ⊢ Ⅎ𝑠(𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)
38		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑧(𝑠 ≠ ∅ → (𝐹‘𝑠) ∈ 𝑠)
39		neeq1 2992	. . . . . . 7 ⊢ (𝑧 = 𝑠 → (𝑧 ≠ ∅ ↔ 𝑠 ≠ ∅))
40		fveq2 6832	. . . . . . . 8 ⊢ (𝑧 = 𝑠 → (𝐹‘𝑧) = (𝐹‘𝑠))
41		id 22	. . . . . . . 8 ⊢ (𝑧 = 𝑠 → 𝑧 = 𝑠)
42	40, 41	eleq12d 2828	. . . . . . 7 ⊢ (𝑧 = 𝑠 → ((𝐹‘𝑧) ∈ 𝑧 ↔ (𝐹‘𝑠) ∈ 𝑠))
43	39, 42	imbi12d 344	. . . . . 6 ⊢ (𝑧 = 𝑠 → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ (𝑠 ≠ ∅ → (𝐹‘𝑠) ∈ 𝑠)))
44	37, 38, 43	cbvralw 3276	. . . . 5 ⊢ (∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ ∀𝑠 ∈ 𝐴 (𝑠 ≠ ∅ → (𝐹‘𝑠) ∈ 𝑠))
45	30, 44	sylibr 234	. . . 4 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) → ∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
46		fveq1 6831	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑧) = (𝐹‘𝑧))
47	46	eleq1d 2819	. . . . . 6 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝐹‘𝑧) ∈ 𝑧))
48	47	imbi2d 340	. . . . 5 ⊢ (𝑓 = 𝐹 → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)))
49	48	ralbidv 3157	. . . 4 ⊢ (𝑓 = 𝐹 → (∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)))
50	22, 45, 49	spcedv 3550	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴) → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
51	50	ex 412	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
52	51	exlimdv 1934	1 ⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049  ∃!wreu 3346  Vcvv 3438   ∖ cdif 3896   ⊆ wss 3899  ∅c0 4283  {csn 4578  ∪ cuni 4861   class class class wbr 5096   ↦ cmpt 5177   Se wse 5573   We wwe 5574  ⟶wf 6486  ‘cfv 6490  ℩crio 7312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-po 5530  df-so 5531  df-fr 5575  df-se 5576  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-riota 7313

This theorem is referenced by:  dfac8c  9941