dfac5lem5

	Ref	Expression
Hypotheses	dfac5lem.1	⊢ 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) }
	dfac5lem.2	⊢ ( 𝜑 ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
	dfac5lem.3	⊢ 𝐵 = ( ∪ 𝐴 ∩ 𝑦 )
Assertion	dfac5lem5	⊢ ( 𝜑 → ∃ 𝑓 ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )

Proof

Step	Hyp	Ref	Expression
1		dfac5lem.1	⊢ 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) }
2		dfac5lem.2	⊢ ( 𝜑 ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
3		dfac5lem.3	⊢ 𝐵 = ( ∪ 𝐴 ∩ 𝑦 )
4	1 2	dfac5lem4	⊢ ( 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
5		simpr	⊢ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ ) → 𝑤 ∈ ℎ )
6	5	a1i	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ ) → 𝑤 ∈ ℎ ) )
7		ineq1	⊢ ( 𝑧 = ( { 𝑤 } × 𝑤 ) → ( 𝑧 ∩ 𝑦 ) = ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) )
8	7	eleq2d	⊢ ( 𝑧 = ( { 𝑤 } × 𝑤 ) → ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑣 ∈ ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) ) )
9	8	eubidv	⊢ ( 𝑧 = ( { 𝑤 } × 𝑤 ) → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) ) )
10	9	rspccv	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ( ( { 𝑤 } × 𝑤 ) ∈ 𝐴 → ∃! 𝑣 𝑣 ∈ ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) ) )
11	1	dfac5lem3	⊢ ( ( { 𝑤 } × 𝑤 ) ∈ 𝐴 ↔ ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ ) )
12		dfac5lem1	⊢ ( ∃! 𝑣 𝑣 ∈ ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) ↔ ∃! 𝑔 ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) )
13	10 11 12	3imtr3g	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ ) → ∃! 𝑔 ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
14	6 13	jcad	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ ) → ( 𝑤 ∈ ℎ ∧ ∃! 𝑔 ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) ) )
15	3	eleq2i	⊢ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ↔ ⟨ 𝑤 , 𝑔 ⟩ ∈ ( ∪ 𝐴 ∩ 𝑦 ) )
16		elin	⊢ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ ( ∪ 𝐴 ∩ 𝑦 ) ↔ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) )
17	1	dfac5lem2	⊢ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ ∪ 𝐴 ↔ ( 𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤 ) )
18	17	anbi1i	⊢ ( ( ⟨ 𝑤 , 𝑔 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ↔ ( ( 𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤 ) ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) )
19		anass	⊢ ( ( ( 𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤 ) ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ↔ ( 𝑤 ∈ ℎ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
20	18 19	bitri	⊢ ( ( ⟨ 𝑤 , 𝑔 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ↔ ( 𝑤 ∈ ℎ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
21	15 16 20	3bitri	⊢ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ↔ ( 𝑤 ∈ ℎ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
22	21	eubii	⊢ ( ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ↔ ∃! 𝑔 ( 𝑤 ∈ ℎ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
23		euanv	⊢ ( ∃! 𝑔 ( 𝑤 ∈ ℎ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) ↔ ( 𝑤 ∈ ℎ ∧ ∃! 𝑔 ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
24	22 23	bitr2i	⊢ ( ( 𝑤 ∈ ℎ ∧ ∃! 𝑔 ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) ↔ ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 )
25	14 24	imbitrdi	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ ) → ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ) )
26		euex	⊢ ( ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ∃ 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 )
27		nfeu1	⊢ Ⅎ 𝑔 ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵
28		nfv	⊢ Ⅎ 𝑔 ( 𝐵 ‘ 𝑤 ) ∈ 𝑤
29	27 28	nfim	⊢ Ⅎ 𝑔 ( ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 )
30	21	simprbi	⊢ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) )
31	30	simpld	⊢ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → 𝑔 ∈ 𝑤 )
32		tz6.12	⊢ ( ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ∧ ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ) → ( 𝐵 ‘ 𝑤 ) = 𝑔 )
33	32	eleq1d	⊢ ( ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ∧ ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ) → ( ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ↔ 𝑔 ∈ 𝑤 ) )
34	33	biimparc	⊢ ( ( 𝑔 ∈ 𝑤 ∧ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ∧ ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 ) ) → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 )
35	34	exp32	⊢ ( 𝑔 ∈ 𝑤 → ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ( ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) ) )
36	31 35	mpcom	⊢ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ( ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) )
37	29 36	exlimi	⊢ ( ∃ 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ( ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) )
38	26 37	mpcom	⊢ ( ∃! 𝑔 ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐵 → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 )
39	25 38	syl6	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ ) → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) )
40	39	expcomd	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ( 𝑤 ∈ ℎ → ( 𝑤 ≠ ∅ → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) ) )
41	40	ralrimiv	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) )
42		vex	⊢ 𝑦 ∈ V
43	42	inex2	⊢ ( ∪ 𝐴 ∩ 𝑦 ) ∈ V
44	3 43	eqeltri	⊢ 𝐵 ∈ V
45		fveq1	⊢ ( 𝑓 = 𝐵 → ( 𝑓 ‘ 𝑤 ) = ( 𝐵 ‘ 𝑤 ) )
46	45	eleq1d	⊢ ( 𝑓 = 𝐵 → ( ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ↔ ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) )
47	46	imbi2d	⊢ ( 𝑓 = 𝐵 → ( ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) ↔ ( 𝑤 ≠ ∅ → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) ) )
48	47	ralbidv	⊢ ( 𝑓 = 𝐵 → ( ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) ↔ ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) ) )
49	44 48	spcev	⊢ ( ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝐵 ‘ 𝑤 ) ∈ 𝑤 ) → ∃ 𝑓 ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
50	41 49	syl	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ∃ 𝑓 ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
51	50	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → ∃ 𝑓 ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
52	4 51	syl	⊢ ( 𝜑 → ∃ 𝑓 ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )

Metamath Proof Explorer

Theorem dfac5lem5

Proof