Theorem fununi 5256

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 5205	. . . . 5 ⊢ (Fun 𝑓 → Rel 𝑓)
2	1	adantr 274	. . . 4 ⊢ ((Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Rel 𝑓)
3	2	ralimi 2529	. . 3 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑓 ∈ 𝐴 Rel 𝑓)
4		reluni 4727	. . 3 ⊢ (Rel ∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓)
5	3, 4	sylibr 133	. 2 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Rel ∪ 𝐴)
6		r19.28av 2602	. . . 4 ⊢ ((Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)))
7	6	ralimi 2529	. . 3 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)))
8		ssel 3136	. . . . . . . . . . . . 13 ⊢ (𝑤 ⊆ 𝑣 → (⟨𝑥, 𝑦⟩ ∈ 𝑤 → ⟨𝑥, 𝑦⟩ ∈ 𝑣))
9	8	anim1d 334	. . . . . . . . . . . 12 ⊢ (𝑤 ⊆ 𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → (⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
10		dffun4 5199	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑣 ↔ (Rel 𝑣 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
11	10	simprbi 273	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑣 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
12	11	19.21bbi 1547	. . . . . . . . . . . . 13 ⊢ (Fun 𝑣 → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
13	12	19.21bi 1546	. . . . . . . . . . . 12 ⊢ (Fun 𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
14	9, 13	syl9r 73	. . . . . . . . . . 11 ⊢ (Fun 𝑣 → (𝑤 ⊆ 𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
15	14	adantl 275	. . . . . . . . . 10 ⊢ ((Fun 𝑤 ∧ Fun 𝑣) → (𝑤 ⊆ 𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
16		ssel 3136	. . . . . . . . . . . . 13 ⊢ (𝑣 ⊆ 𝑤 → (⟨𝑥, 𝑧⟩ ∈ 𝑣 → ⟨𝑥, 𝑧⟩ ∈ 𝑤))
17	16	anim2d 335	. . . . . . . . . . . 12 ⊢ (𝑣 ⊆ 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤)))
18		dffun4 5199	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑤 ↔ (Rel 𝑤 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧)))
19	18	simprbi 273	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑤 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧))
20	19	19.21bbi 1547	. . . . . . . . . . . . 13 ⊢ (Fun 𝑤 → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧))
21	20	19.21bi 1546	. . . . . . . . . . . 12 ⊢ (Fun 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧))
22	17, 21	syl9r 73	. . . . . . . . . . 11 ⊢ (Fun 𝑤 → (𝑣 ⊆ 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
23	22	adantr 274	. . . . . . . . . 10 ⊢ ((Fun 𝑤 ∧ Fun 𝑣) → (𝑣 ⊆ 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
24	15, 23	jaod 707	. . . . . . . . 9 ⊢ ((Fun 𝑤 ∧ Fun 𝑣) → ((𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
25	24	imp 123	. . . . . . . 8 ⊢ (((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
26	25	ralimi 2529	. . . . . . 7 ⊢ (∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) → ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
27	26	ralimi 2529	. . . . . 6 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) → ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
28		funeq 5208	. . . . . . . . . 10 ⊢ (𝑓 = 𝑤 → (Fun 𝑓 ↔ Fun 𝑤))
29		sseq1 3165	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑤 → (𝑓 ⊆ 𝑔 ↔ 𝑤 ⊆ 𝑔))
30		sseq2 3166	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑤 → (𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑤))
31	29, 30	orbi12d 783	. . . . . . . . . 10 ⊢ (𝑓 = 𝑤 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤)))
32	28, 31	anbi12d 465	. . . . . . . . 9 ⊢ (𝑓 = 𝑤 → ((Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun 𝑤 ∧ (𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤))))
33		sseq2 3166	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑣 → (𝑤 ⊆ 𝑔 ↔ 𝑤 ⊆ 𝑣))
34		sseq1 3165	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑣 → (𝑔 ⊆ 𝑤 ↔ 𝑣 ⊆ 𝑤))
35	33, 34	orbi12d 783	. . . . . . . . . 10 ⊢ (𝑔 = 𝑣 → ((𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤) ↔ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
36	35	anbi2d 460	. . . . . . . . 9 ⊢ (𝑔 = 𝑣 → ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤)) ↔ (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
37	32, 36	cbvral2v 2705	. . . . . . . 8 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
38		ralcom 2629	. . . . . . . . 9 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑔 ∈ 𝐴 ∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)))
39		orcom 718	. . . . . . . . . . . 12 ⊢ ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑔 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑔))
40		sseq1 3165	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑤 → (𝑔 ⊆ 𝑓 ↔ 𝑤 ⊆ 𝑓))
41		sseq2 3166	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑤 → (𝑓 ⊆ 𝑔 ↔ 𝑓 ⊆ 𝑤))
42	40, 41	orbi12d 783	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑤 → ((𝑔 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑔) ↔ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤)))
43	39, 42	syl5bb 191	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑤 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤)))
44	43	anbi2d 460	. . . . . . . . . 10 ⊢ (𝑔 = 𝑤 → ((Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun 𝑓 ∧ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤))))
45		funeq 5208	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → (Fun 𝑓 ↔ Fun 𝑣))
46		sseq2 3166	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑤 ⊆ 𝑓 ↔ 𝑤 ⊆ 𝑣))
47		sseq1 3165	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑓 ⊆ 𝑤 ↔ 𝑣 ⊆ 𝑤))
48	46, 47	orbi12d 783	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ((𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤) ↔ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
49	45, 48	anbi12d 465	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → ((Fun 𝑓 ∧ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤)) ↔ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
50	44, 49	cbvral2v 2705	. . . . . . . . 9 ⊢ (∀𝑔 ∈ 𝐴 ∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
51	38, 50	bitri 183	. . . . . . . 8 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
52	37, 51	anbi12i 456	. . . . . . 7 ⊢ ((∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) ↔ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
53		anidm 394	. . . . . . 7 ⊢ ((∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) ↔ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)))
54		anandir 581	. . . . . . . . 9 ⊢ (((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ↔ ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
55	54	2ralbii 2474	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
56		r19.26-2 2595	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) ↔ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))))
57	55, 56	bitr2i 184	. . . . . . 7 ⊢ ((∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
58	52, 53, 57	3bitr3i 209	. . . . . 6 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))
59		eluni 3792	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃𝑤(⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴))
60		eluni 3792	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑣(⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴))
61	59, 60	anbi12i 456	. . . . . . . . 9 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) ↔ (∃𝑤(⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ ∃𝑣(⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)))
62		eeanv 1920	. . . . . . . . 9 ⊢ (∃𝑤∃𝑣((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ (∃𝑤(⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ ∃𝑣(⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)))
63		an4 576	. . . . . . . . . . 11 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)))
64		ancom 264	. . . . . . . . . . 11 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
65	63, 64	bitri 183	. . . . . . . . . 10 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
66	65	2exbii 1594	. . . . . . . . 9 ⊢ (∃𝑤∃𝑣((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ ∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
67	61, 62, 66	3bitr2i 207	. . . . . . . 8 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) ↔ ∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
68	67	imbi1i 237	. . . . . . 7 ⊢ (((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧) ↔ (∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
69		19.23v 1871	. . . . . . 7 ⊢ (∀𝑤(∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ (∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
70		r2al 2485	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧) ↔ ∀𝑤∀𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
71		impexp 261	. . . . . . . . 9 ⊢ ((((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
72	71	2albii 1459	. . . . . . . 8 ⊢ (∀𝑤∀𝑣(((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤∀𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
73		19.23v 1871	. . . . . . . . 9 ⊢ (∀𝑣(((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ (∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
74	73	albii 1458	. . . . . . . 8 ⊢ (∀𝑤∀𝑣(((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤(∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
75	70, 72, 74	3bitr2ri 208	. . . . . . 7 ⊢ (∀𝑤(∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
76	68, 69, 75	3bitr2i 207	. . . . . 6 ⊢ (((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
77	27, 58, 76	3imtr4i 200	. . . . 5 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
78	77	alrimiv 1862	. . . 4 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
79	78	alrimivv 1863	. . 3 ⊢ (∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
80	7, 79	syl 14	. 2 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
81		dffun4 5199	. 2 ⊢ (Fun ∪ 𝐴 ↔ (Rel ∪ 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)))
82	5, 80, 81	sylanbrc 414	1 ⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ 𝐴)

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 698  ∀wal 1341  ∃wex 1480   ∈ wcel 2136  ∀wral 2444   ⊆ wss 3116  ⟨cop 3579  ∪ cuni 3789  Rel wrel 4609  Fun wfun 5182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-pow 4153  ax-pr 4187

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-rex 2450  df-v 2728  df-un 3120  df-in 3122  df-ss 3129  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-iun 3868  df-br 3983  df-opab 4044  df-id 4271  df-rel 4611  df-cnv 4612  df-co 4613  df-fun 5190

This theorem is referenced by:  funcnvuni  5257  fun11uni  5258  ennnfonelemfun  12350