Theorem fun11iun 7126

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 3203	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
2		eqeq1 2626	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝑧 = 𝐵 ↔ 𝑢 = 𝐵))
3	2	rexbidv 3052	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵))
4	1, 3	elab 3350	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵)
5		r19.29 3072	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵))
6		nfv 1843	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(Fun 𝑢 ∧ Fun ◡𝑢)
7		nfre1 3005	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵
8	7	nfab 2769	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
9		nfv 1843	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
10	8, 9	nfral 2945	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
11	6, 10	nfan 1828	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
12		f1eq1 6096	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝐵 → (𝑢:𝐷–1-1→𝑆 ↔ 𝐵:𝐷–1-1→𝑆))
13	12	biimparc 504	. . . . . . . . . . . . . . 15 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → 𝑢:𝐷–1-1→𝑆)
14		df-f1 5893	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:𝐷–1-1→𝑆 ↔ (𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢))
15		ffun 6048	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢:𝐷⟶𝑆 → Fun 𝑢)
16	15	anim1i 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢) → (Fun 𝑢 ∧ Fun ◡𝑢))
17	14, 16	sylbi 207	. . . . . . . . . . . . . . 15 ⊢ (𝑢:𝐷–1-1→𝑆 → (Fun 𝑢 ∧ Fun ◡𝑢))
18	13, 17	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢))
19	18	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢))
20		vex 3203	. . . . . . . . . . . . . . . 16 ⊢ 𝑣 ∈ V
21		eqeq1 2626	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑣 → (𝑧 = 𝐵 ↔ 𝑣 = 𝐵))
22	21	rexbidv 3052	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑣 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑣 = 𝐵))
23	20, 22	elab 3350	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑣 = 𝐵)
24		fun11iun.1	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
25	24	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑣 = 𝐵 ↔ 𝑣 = 𝐶))
26	25	cbvrexv 3172	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥 ∈ 𝐴 𝑣 = 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶)
27		r19.29 3072	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶) → ∃𝑦 ∈ 𝐴 ((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑣 = 𝐶))
28		sseq12 3628	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 = 𝐵 ∧ 𝑣 = 𝐶) → (𝑢 ⊆ 𝑣 ↔ 𝐵 ⊆ 𝐶))
29	28	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 = 𝐶 ∧ 𝑢 = 𝐵) → (𝑢 ⊆ 𝑣 ↔ 𝐵 ⊆ 𝐶))
30		sseq12 3628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 = 𝐶 ∧ 𝑢 = 𝐵) → (𝑣 ⊆ 𝑢 ↔ 𝐶 ⊆ 𝐵))
31	29, 30	orbi12d 746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 = 𝐶 ∧ 𝑢 = 𝐵) → ((𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢) ↔ (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)))
32	31	biimprcd 240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) → ((𝑣 = 𝐶 ∧ 𝑢 = 𝐵) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
33	32	expdimp 453	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑣 = 𝐶) → (𝑢 = 𝐵 → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
34	33	rexlimivw 3029	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦 ∈ 𝐴 ((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑣 = 𝐶) → (𝑢 = 𝐵 → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
35	34	imp 445	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑦 ∈ 𝐴 ((𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑣 = 𝐶) ∧ 𝑢 = 𝐵) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
36	27, 35	sylan 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶) ∧ 𝑢 = 𝐵) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
37	36	an32s 846	. . . . . . . . . . . . . . . . 17 ⊢ (((∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵) ∧ 𝑢 = 𝐵) ∧ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
38	37	adantlll 754	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) ∧ ∃𝑦 ∈ 𝐴 𝑣 = 𝐶) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
39	26, 38	sylan2b 492	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) ∧ ∃𝑥 ∈ 𝐴 𝑣 = 𝐵) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
40	23, 39	sylan2b 492	. . . . . . . . . . . . . 14 ⊢ ((((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
41	40	ralrimiva 2966	. . . . . . . . . . . . 13 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
42	19, 41	jca 554	. . . . . . . . . . . 12 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
43	42	a1i 11	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
44	11, 43	rexlimi 3024	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
45	5, 44	syl 17	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
46	4, 45	sylan2b 492	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
47	46	ralrimiva 2966	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
48		fun11uni 7120	. . . . . . 7 ⊢ (∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → (Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}))
49	47, 48	syl 17	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}))
50	49	simpld 475	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
51		fun11iun.2	. . . . . . 7 ⊢ 𝐵 ∈ V
52	51	dfiun2 4554	. . . . . 6 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
53	52	funeqi 5909	. . . . 5 ⊢ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
54	50, 53	sylibr 224	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ 𝑥 ∈ 𝐴 𝐵)
55		nfra1 2941	. . . . . . 7 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵))
56		rsp 2929	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑥 ∈ 𝐴 → (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵))))
57	1	eldm2 5322	. . . . . . . . . . 11 ⊢ (𝑢 ∈ dom 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
58		f1dm 6105	. . . . . . . . . . . 12 ⊢ (𝐵:𝐷–1-1→𝑆 → dom 𝐵 = 𝐷)
59	58	eleq2d 2687	. . . . . . . . . . 11 ⊢ (𝐵:𝐷–1-1→𝑆 → (𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷))
60	57, 59	syl5bbr 274	. . . . . . . . . 10 ⊢ (𝐵:𝐷–1-1→𝑆 → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
61	60	adantr 481	. . . . . . . . 9 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
62	56, 61	syl6 35	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑥 ∈ 𝐴 → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷)))
63	62	imp 445	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
64	55, 63	rexbida 3047	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷))
65		eliun 4524	. . . . . . . 8 ⊢ (⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
66	65	exbii 1774	. . . . . . 7 ⊢ (∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
67	1	eldm2 5322	. . . . . . 7 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
68		rexcom4 3225	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
69	66, 67, 68	3bitr4i 292	. . . . . 6 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
70		eliun 4524	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷)
71	64, 69, 70	3bitr4g 303	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷))
72	71	eqrdv 2620	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷)
73		df-fn 5891	. . . 4 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ↔ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷))
74	54, 72, 73	sylanbrc 698	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷)
75		rniun 5543	. . . 4 ⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
76		f1f 6101	. . . . . . . 8 ⊢ (𝐵:𝐷–1-1→𝑆 → 𝐵:𝐷⟶𝑆)
77		frn 6053	. . . . . . . 8 ⊢ (𝐵:𝐷⟶𝑆 → ran 𝐵 ⊆ 𝑆)
78	76, 77	syl 17	. . . . . . 7 ⊢ (𝐵:𝐷–1-1→𝑆 → ran 𝐵 ⊆ 𝑆)
79	78	adantr 481	. . . . . 6 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran 𝐵 ⊆ 𝑆)
80	79	ralimi 2952	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
81		iunss 4561	. . . . 5 ⊢ (∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
82	80, 81	sylibr 224	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
83	75, 82	syl5eqss 3649	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆)
84		df-f 5892	. . 3 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆))
85	74, 83, 84	sylanbrc 698	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆)
86	49	simprd 479	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
87	52	cnveqi 5297	. . . 4 ⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
88	87	funeqi 5909	. . 3 ⊢ (Fun ◡∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
89	86, 88	sylibr 224	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ 𝑥 ∈ 𝐴 𝐵)
90		df-f1 5893	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ∧ Fun ◡∪ 𝑥 ∈ 𝐴 𝐵))
91	85, 89, 90	sylanbrc 698	1 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆)

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  {cab 2608  ∀wral 2912  ∃wrex 2913  Vcvv 3200   ⊆ wss 3574  ⟨cop 4183  ∪ cuni 4436  ∪ ciun 4520  ^◡ccnv 5113  dom cdm 5114  ran crn 5115  Fun wfun 5882   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893

This theorem is referenced by:  ackbij2  9065