Theorem ac6c4

Description: Equivalent of Axiom of Choice. B is a collection B ( x ) of nonempty sets. (Contributed by Mario Carneiro, 22-Mar-2013)

	Ref	Expression
Hypotheses	ac6c4.1	⊢ 𝐴 ∈ V
	ac6c4.2	⊢ 𝐵 ∈ V
Assertion	ac6c4	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ac6c4.1	⊢ 𝐴 ∈ V
2		ac6c4.2	⊢ 𝐵 ∈ V
3		nfv	⊢ Ⅎ 𝑧 𝐵 ≠ ∅
4		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
5		nfcv	⊢ Ⅎ 𝑥 ∅
6	4 5	nfne	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ≠ ∅
7		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
8	7	neeq1d	⊢ ( 𝑥 = 𝑧 → ( 𝐵 ≠ ∅ ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ≠ ∅ ) )
9	3 6 8	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ↔ ∀ 𝑧 ∈ 𝐴 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ≠ ∅ )
10		n0	⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
11		nfv	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐴
12		nfre1	⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵
13	4	nfel2	⊢ Ⅎ 𝑥 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵
14	7	eleq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
15	13 14	rspce	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
16		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
17	15 16	sylibr	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
18		rspe	⊢ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
19	17 18	sylancom	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
20	19	ex	⊢ ( 𝑧 ∈ 𝐴 → ( 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 → ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
21	11 12 20	exlimd	⊢ ( 𝑧 ∈ 𝐴 → ( ∃ 𝑦 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 → ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
22	10 21	syl5bi	⊢ ( 𝑧 ∈ 𝐴 → ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ≠ ∅ → ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
23	22	ralimia	⊢ ( ∀ 𝑧 ∈ 𝐴 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ≠ ∅ → ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
24	9 23	sylbi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
25	1 2	iunex	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V
26		eleq1	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑧 ) → ( 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↔ ( 𝑓 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
27	1 25 26	ac6	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
28		ffn	⊢ ( 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑓 Fn 𝐴 )
29		nfv	⊢ Ⅎ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵
30	4	nfel2	⊢ Ⅎ 𝑥 ( 𝑓 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵
31		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑧 ) )
32	31 7	eleq12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑓 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
33	29 30 32	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
34	33	biimpri	⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
35	28 34	anim12i	⊢ ( ( 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
36	35	eximi	⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
37	24 27 36	3syl	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )