Theorem fun11iun 5601

Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.)

Hypotheses

Ref	Expression
fun11iun.1	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
fun11iun.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
fun11iun	⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝑆

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)   𝐷(𝑥,𝑦)   𝑆(𝑦)

Proof of Theorem fun11iun

Dummy variables 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2803	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
2		eqeq1 2236	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝑧 = 𝐵 ↔ 𝑢 = 𝐵))
3	2	rexbidv 2531	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵))
4	1, 3	elab 2948	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵)
5		r19.29 2668	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵))
6		nfv 1574	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(Fun 𝑢 ∧ Fun ◡𝑢)
7		nfre1 2573	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵
8	7	nfab 2377	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
9		nfv 1574	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
10	8, 9	nfralxy 2568	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
11	6, 10	nfan 1611	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
12		f1eq1 5534	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝐵 → (𝑢:𝐷–1-1→𝑆 ↔ 𝐵:𝐷–1-1→𝑆))
13	12	biimparc 299	. . . . . . . . . . . . . . 15 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → 𝑢:𝐷–1-1→𝑆)
14		df-f1 5329	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:𝐷–1-1→𝑆 ↔ (𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢))
15		ffun 5482	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢:𝐷⟶𝑆 → Fun 𝑢)
16	15	anim1i 340	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢) → (Fun 𝑢 ∧ Fun ◡𝑢))
17	14, 16	sylbi 121	. . . . . . . . . . . . . . 15 ⊢ (𝑢:𝐷–1-1→𝑆 → (Fun 𝑢 ∧ Fun ◡𝑢))
18	13, 17	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢))
19	18	adantlr 477	. . . . . . . . . . . . 13 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢))
20		vex 2803	. . . . . . . . . . . . . . . 16 ⊢ 𝑣 ∈ V
21		eqeq1 2236	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑣 → (𝑧 = 𝐵 ↔ 𝑣 = 𝐵))
22	21	rexbidv 2531	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑣 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑣 = 𝐵))
23	20, 22	elab 2948	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑣 = 𝐵)
24		fun11iun.1	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
25	24	eqeq2d 2241	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑣 = 𝐵 ↔ 𝑣 = 𝐶))
26	25	cbvrexv 2766	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥 ∈ 𝐴 𝑣 = 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶)
27		r19.29 2668	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶) → ∃𝑦 ∈ 𝐴 ((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑣 = 𝐶))
28		sseq12 3250	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 = 𝐵 ∧ 𝑣 = 𝐶) → (𝑢 ⊆ 𝑣 ↔ 𝐵 ⊆ 𝐶))
29	28	ancoms 268	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 = 𝐶 ∧ 𝑢 = 𝐵) → (𝑢 ⊆ 𝑣 ↔ 𝐵 ⊆ 𝐶))
30		sseq12 3250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 = 𝐶 ∧ 𝑢 = 𝐵) → (𝑣 ⊆ 𝑢 ↔ 𝐶 ⊆ 𝐵))
31	29, 30	orbi12d 798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 = 𝐶 ∧ 𝑢 = 𝐵) → ((𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢) ↔ (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)))
32	31	biimprcd 160	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) → ((𝑣 = 𝐶 ∧ 𝑢 = 𝐵) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
33	32	expdimp 259	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑣 = 𝐶) → (𝑢 = 𝐵 → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
34	33	rexlimivw 2644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦 ∈ 𝐴 ((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑣 = 𝐶) → (𝑢 = 𝐵 → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
35	34	imp 124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑦 ∈ 𝐴 ((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑣 = 𝐶) ∧ 𝑢 = 𝐵) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
36	27, 35	sylan 283	. . . . . . . . . . . . . . . . . 18 ⊢ (((∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶) ∧ 𝑢 = 𝐵) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
37	36	an32s 568	. . . . . . . . . . . . . . . . 17 ⊢ (((∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑢 = 𝐵) ∧ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
38	37	adantlll 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) ∧ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
39	26, 38	sylan2b 287	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) ∧ ∃𝑥 ∈ 𝐴 𝑣 = 𝐵) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
40	23, 39	sylan2b 287	. . . . . . . . . . . . . 14 ⊢ ((((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
41	40	ralrimiva 2603	. . . . . . . . . . . . 13 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
42	19, 41	jca 306	. . . . . . . . . . . 12 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
43	42	a1i 9	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
44	11, 43	rexlimi 2641	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
45	5, 44	syl 14	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
46	4, 45	sylan2b 287	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
47	46	ralrimiva 2603	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
48		fun11uni 5397	. . . . . . 7 ⊢ (∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → (Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}))
49	47, 48	syl 14	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}))
50	49	simpld 112	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
51		fun11iun.2	. . . . . . 7 ⊢ 𝐵 ∈ V
52	51	dfiun2 4002	. . . . . 6 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
53	52	funeqi 5345	. . . . 5 ⊢ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
54	50, 53	sylibr 134	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ 𝑥 ∈ 𝐴 𝐵)
55		nfra1 2561	. . . . . . 7 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵))
56		rsp 2577	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑥 ∈ 𝐴 → (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵))))
57	1	eldm2 4927	. . . . . . . . . . 11 ⊢ (𝑢 ∈ dom 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
58		f1dm 5544	. . . . . . . . . . . 12 ⊢ (𝐵:𝐷–1-1→𝑆 → dom 𝐵 = 𝐷)
59	58	eleq2d 2299	. . . . . . . . . . 11 ⊢ (𝐵:𝐷–1-1→𝑆 → (𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷))
60	57, 59	bitr3id 194	. . . . . . . . . 10 ⊢ (𝐵:𝐷–1-1→𝑆 → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
61	60	adantr 276	. . . . . . . . 9 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
62	56, 61	syl6 33	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑥 ∈ 𝐴 → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷)))
63	62	imp 124	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
64	55, 63	rexbida 2525	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷))
65		eliun 3972	. . . . . . . 8 ⊢ (⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
66	65	exbii 1651	. . . . . . 7 ⊢ (∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
67	1	eldm2 4927	. . . . . . 7 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
68		rexcom4 2824	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
69	66, 67, 68	3bitr4i 212	. . . . . 6 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
70		eliun 3972	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷)
71	64, 69, 70	3bitr4g 223	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷))
72	71	eqrdv 2227	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷)
73		df-fn 5327	. . . 4 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ↔ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷))
74	54, 72, 73	sylanbrc 417	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷)
75		rniun 5145	. . . 4 ⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
76		f1rn 5540	. . . . . . 7 ⊢ (𝐵:𝐷–1-1→𝑆 → ran 𝐵 ⊆ 𝑆)
77	76	adantr 276	. . . . . 6 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran 𝐵 ⊆ 𝑆)
78	77	ralimi 2593	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
79		iunss 4009	. . . . 5 ⊢ (∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
80	78, 79	sylibr 134	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
81	75, 80	eqsstrid 3271	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆)
82		df-f 5328	. . 3 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆))
83	74, 81, 82	sylanbrc 417	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆)
84	49	simprd 114	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
85	52	cnveqi 4903	. . . 4 ⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
86	85	funeqi 5345	. . 3 ⊢ (Fun ◡∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
87	84, 86	sylibr 134	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ 𝑥 ∈ 𝐴 𝐵)
88		df-f1 5329	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ∧ Fun ◡∪ 𝑥 ∈ 𝐴 𝐵))
89	83, 87, 88	sylanbrc 417	1 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 713   = wceq 1395  ∃wex 1538   ∈ wcel 2200  {cab 2215  ∀wral 2508  ∃wrex 2509  Vcvv 2800   ⊆ wss 3198  ⟨cop 3670  ∪ cuni 3891  ∪ ciun 3968  ^◡ccnv 4722  dom cdm 4723  ran crn 4724  Fun wfun 5318   Fn wfn 5319  ⟶wf 5320  –1-1→wf1 5321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-iun 3970  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-fun 5326  df-fn 5327  df-f 5328  df-f1 5329

This theorem is referenced by: (None)