Theorem dfac8clem

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

	Ref	Expression
Hypothesis	dfac8clem.1	⊢ 𝐹 = ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ↦ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
Assertion	dfac8clem	⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑟 𝑟 We ∪ 𝐴 → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfac8clem.1	⊢ 𝐹 = ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ↦ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
2		eldifsn	⊢ ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ↔ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) )
3		elssuni	⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ⊆ ∪ 𝐴 )
4	3	ad2antrl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → 𝑠 ⊆ ∪ 𝐴 )
5		simplr	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → 𝑟 We ∪ 𝐴 )
6		vex	⊢ 𝑟 ∈ V
7		exse2	⊢ ( 𝑟 ∈ V → 𝑟 Se ∪ 𝐴 )
8	6 7	mp1i	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → 𝑟 Se ∪ 𝐴 )
9		simprr	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → 𝑠 ≠ ∅ )
10		wereu2	⊢ ( ( ( 𝑟 We ∪ 𝐴 ∧ 𝑟 Se ∪ 𝐴 ) ∧ ( 𝑠 ⊆ ∪ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ∃! 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 )
11	5 8 4 9 10	syl22anc	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ∃! 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 )
12		riotacl	⊢ ( ∃! 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 → ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ 𝑠 )
13	11 12	syl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ 𝑠 )
14	4 13	sseldd	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ ∪ 𝐴 )
15	2 14	sylan2b	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ) → ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ ∪ 𝐴 )
16	15 1	fmptd	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → 𝐹 : ( 𝐴 ∖ { ∅ } ) ⟶ ∪ 𝐴 )
17		difexg	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∖ { ∅ } ) ∈ V )
18	17	adantr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ( 𝐴 ∖ { ∅ } ) ∈ V )
19		uniexg	⊢ ( 𝐴 ∈ 𝐵 → ∪ 𝐴 ∈ V )
20	19	adantr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ∪ 𝐴 ∈ V )
21		fex2	⊢ ( ( 𝐹 : ( 𝐴 ∖ { ∅ } ) ⟶ ∪ 𝐴 ∧ ( 𝐴 ∖ { ∅ } ) ∈ V ∧ ∪ 𝐴 ∈ V ) → 𝐹 ∈ V )
22	16 18 20 21	syl3anc	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → 𝐹 ∈ V )
23		riotaex	⊢ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ V
24	1	fvmpt2	⊢ ( ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ∧ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ V ) → ( 𝐹 ‘ 𝑠 ) = ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
25	23 24	mpan2	⊢ ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) → ( 𝐹 ‘ 𝑠 ) = ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
26	2 25	sylbir	⊢ ( ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) → ( 𝐹 ‘ 𝑠 ) = ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
27	26	adantl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑠 ) = ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
28	27 13	eqeltrd	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 )
29	28	expr	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) )
30	29	ralrimiva	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ∀ 𝑠 ∈ 𝐴 ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) )
31		nfv	⊢ Ⅎ 𝑠 𝑧 ≠ ∅
32		nfmpt1	⊢ Ⅎ 𝑠 ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ↦ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
33	1 32	nfcxfr	⊢ Ⅎ 𝑠 𝐹
34		nfcv	⊢ Ⅎ 𝑠 𝑧
35	33 34	nffv	⊢ Ⅎ 𝑠 ( 𝐹 ‘ 𝑧 )
36	35	nfel1	⊢ Ⅎ 𝑠 ( 𝐹 ‘ 𝑧 ) ∈ 𝑧
37	31 36	nfim	⊢ Ⅎ 𝑠 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 )
38		nfv	⊢ Ⅎ 𝑧 ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 )
39		neeq1	⊢ ( 𝑧 = 𝑠 → ( 𝑧 ≠ ∅ ↔ 𝑠 ≠ ∅ ) )
40		fveq2	⊢ ( 𝑧 = 𝑠 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑠 ) )
41		id	⊢ ( 𝑧 = 𝑠 → 𝑧 = 𝑠 )
42	40 41	eleq12d	⊢ ( 𝑧 = 𝑠 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) )
43	39 42	imbi12d	⊢ ( 𝑧 = 𝑠 → ( ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) ) )
44	37 38 43	cbvralw	⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑠 ∈ 𝐴 ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) )
45	30 44	sylibr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
46		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
47	46	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
48	47	imbi2d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ) )
49	48	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ) )
50	22 45 49	spcedv	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
51	50	ex	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑟 We ∪ 𝐴 → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
52	51	exlimdv	⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑟 𝑟 We ∪ 𝐴 → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )