Theorem fununi 5449

Description: The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.)

Assertion

Ref	Expression
fununi	⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ 𝐴)

Distinct variable group:   𝑓,𝑔,𝐴

Proof of Theorem fununi

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funrel 5394	. . . . 5 ⊢ (Fun 𝑓 → Rel 𝑓)
2	1	adantr 276	. . . 4 ⊢ ((Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Rel 𝑓)
3	2	ralimi 2613	. . 3 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑓 ∈ 𝐴 Rel 𝑓)
4		reluni 4900	. . 3 ⊢ (Rel ∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓)
5	3, 4	sylibr 134	. 2 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Rel ∪ 𝐴)
6		r19.28av 2687	. . . 4 ⊢ ((Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)))
7	6	ralimi 2613	. . 3 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)))
8		ssel 3242	. . . . . . . . . . . . 13 ⊢ (𝑤 ⊆ 𝑣 → (⟨𝑥, 𝑦⟩ ∈ 𝑤 → ⟨𝑥, 𝑦⟩ ∈ 𝑣))
9	8	anim1d 336	. . . . . . . . . . . 12 ⊢ (𝑤 ⊆ 𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → (⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
10		dffun4 5388	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑣 ↔ (Rel 𝑣 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
11	10	simprbi 275	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑣 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
12	11	19.21bbi 1612	. . . . . . . . . . . . 13 ⊢ (Fun 𝑣 → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
13	12	19.21bi 1611	. . . . . . . . . . . 12 ⊢ (Fun 𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
14	9, 13	syl9r 73	. . . . . . . . . . 11 ⊢ (Fun 𝑣 → (𝑤 ⊆ 𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
15	14	adantl 277	. . . . . . . . . 10 ⊢ ((Fun 𝑤 ∧ Fun 𝑣) → (𝑤 ⊆ 𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
16		ssel 3242	. . . . . . . . . . . . 13 ⊢ (𝑣 ⊆ 𝑤 → (⟨𝑥, 𝑧⟩ ∈ 𝑣 → ⟨𝑥, 𝑧⟩ ∈ 𝑤))
17	16	anim2d 337	. . . . . . . . . . . 12 ⊢ (𝑣 ⊆ 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤)))
18		dffun4 5388	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑤 ↔ (Rel 𝑤 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧)))
19	18	simprbi 275	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑤 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧))
20	19	19.21bbi 1612	. . . . . . . . . . . . 13 ⊢ (Fun 𝑤 → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧))
21	20	19.21bi 1611	. . . . . . . . . . . 12 ⊢ (Fun 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧))
22	17, 21	syl9r 73	. . . . . . . . . . 11 ⊢ (Fun 𝑤 → (𝑣 ⊆ 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
23	22	adantr 276	. . . . . . . . . 10 ⊢ ((Fun 𝑤 ∧ Fun 𝑣) → (𝑣 ⊆ 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
24	15, 23	jaod 729	. . . . . . . . 9 ⊢ ((Fun 𝑤 ∧ Fun 𝑣) → ((𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
25	24	imp 124	. . . . . . . 8 ⊢ (((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
26	25	ralimi 2613	. . . . . . 7 ⊢ (∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) → ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
27	26	ralimi 2613	. . . . . 6 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) → ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
28		funeq 5397	. . . . . . . . . 10 ⊢ (𝑓 = 𝑤 → (Fun 𝑓 ↔ Fun 𝑤))
29		sseq1 3271	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑤 → (𝑓 ⊆ 𝑔 ↔ 𝑤 ⊆ 𝑔))
30		sseq2 3272	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑤 → (𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑤))
31	29, 30	orbi12d 805	. . . . . . . . . 10 ⊢ (𝑓 = 𝑤 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤)))
32	28, 31	anbi12d 477	. . . . . . . . 9 ⊢ (𝑓 = 𝑤 → ((Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun 𝑤 ∧ (𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤))))
33		sseq2 3272	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑣 → (𝑤 ⊆ 𝑔 ↔ 𝑤 ⊆ 𝑣))
34		sseq1 3271	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑣 → (𝑔 ⊆ 𝑤 ↔ 𝑣 ⊆ 𝑤))
35	33, 34	orbi12d 805	. . . . . . . . . 10 ⊢ (𝑔 = 𝑣 → ((𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤) ↔ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
36	35	anbi2d 468	. . . . . . . . 9 ⊢ (𝑔 = 𝑣 → ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤)) ↔ (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
37	32, 36	cbvral2v 2799	. . . . . . . 8 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
38		ralcom 2714	. . . . . . . . 9 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑔 ∈ 𝐴 ∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)))
39		orcom 740	. . . . . . . . . . . 12 ⊢ ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑔 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑔))
40		sseq1 3271	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑤 → (𝑔 ⊆ 𝑓 ↔ 𝑤 ⊆ 𝑓))
41		sseq2 3272	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑤 → (𝑓 ⊆ 𝑔 ↔ 𝑓 ⊆ 𝑤))
42	40, 41	orbi12d 805	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑤 → ((𝑔 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑔) ↔ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤)))
43	39, 42	bitrid 192	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑤 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤)))
44	43	anbi2d 468	. . . . . . . . . 10 ⊢ (𝑔 = 𝑤 → ((Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun 𝑓 ∧ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤))))
45		funeq 5397	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → (Fun 𝑓 ↔ Fun 𝑣))
46		sseq2 3272	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑤 ⊆ 𝑓 ↔ 𝑤 ⊆ 𝑣))
47		sseq1 3271	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑓 ⊆ 𝑤 ↔ 𝑣 ⊆ 𝑤))
48	46, 47	orbi12d 805	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ((𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤) ↔ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
49	45, 48	anbi12d 477	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → ((Fun 𝑓 ∧ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤)) ↔ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
50	44, 49	cbvral2v 2799	. . . . . . . . 9 ⊢ (∀𝑔 ∈ 𝐴 ∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
51	38, 50	bitri 184	. . . . . . . 8 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
52	37, 51	anbi12i 464	. . . . . . 7 ⊢ ((∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) ↔ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
53		anidm 400	. . . . . . 7 ⊢ ((∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) ↔ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)))
54		anandir 599	. . . . . . . . 9 ⊢ (((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ↔ ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
55	54	2ralbii 2558	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
56		r19.26-2 2680	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) ↔ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
57	55, 56	bitr2i 185	. . . . . . 7 ⊢ ((∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
58	52, 53, 57	3bitr3i 210	. . . . . 6 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
59		eluni 3938	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃𝑤(⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴))
60		eluni 3938	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑣(⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴))
61	59, 60	anbi12i 464	. . . . . . . . 9 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) ↔ (∃𝑤(⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ ∃𝑣(⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)))
62		eeanv 1992	. . . . . . . . 9 ⊢ (∃𝑤∃𝑣((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ (∃𝑤(⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ ∃𝑣(⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)))
63		an4 592	. . . . . . . . . . 11 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)))
64		ancom 266	. . . . . . . . . . 11 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
65	63, 64	bitri 184	. . . . . . . . . 10 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
66	65	2exbii 1659	. . . . . . . . 9 ⊢ (∃𝑤∃𝑣((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ ∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
67	61, 62, 66	3bitr2i 208	. . . . . . . 8 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) ↔ ∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
68	67	imbi1i 238	. . . . . . 7 ⊢ (((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧) ↔ (∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
69		19.23v 1936	. . . . . . 7 ⊢ (∀𝑤(∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ (∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
70		r2al 2569	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧) ↔ ∀𝑤∀𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
71		impexp 263	. . . . . . . . 9 ⊢ ((((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
72	71	2albii 1524	. . . . . . . 8 ⊢ (∀𝑤∀𝑣(((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤∀𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
73		19.23v 1936	. . . . . . . . 9 ⊢ (∀𝑣(((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ (∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
74	73	albii 1523	. . . . . . . 8 ⊢ (∀𝑤∀𝑣(((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤(∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
75	70, 72, 74	3bitr2ri 209	. . . . . . 7 ⊢ (∀𝑤(∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
76	68, 69, 75	3bitr2i 208	. . . . . 6 ⊢ (((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
77	27, 58, 76	3imtr4i 201	. . . . 5 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
78	77	alrimiv 1927	. . . 4 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
79	78	alrimivv 1928	. . 3 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
80	7, 79	syl 14	. 2 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
81		dffun4 5388	. 2 ⊢ (Fun ∪ 𝐴 ↔ (Rel ∪ 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)))
82	5, 80, 81	sylanbrc 421	1 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∨ wo 720  ∀wal 1400  ∃wex 1545   ∈ wcel 2209  ∀wral 2528   ⊆ wss 3220  ⟨cop 3712  ∪ cuni 3935  Rel wrel 4779  Fun wfun 5371

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-iun 4014  df-br 4131  df-opab 4193  df-id 4438  df-rel 4781  df-cnv 4782  df-co 4783  df-fun 5379

This theorem is used by:  funcnvuni  5450  fun11uni  5451  ennnfonelemfun  13360