Theorem fiun

Description: The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun . (Contributed by AV, 6-Oct-2023)

	Ref	Expression
Hypotheses	fiun.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
	fiun.2	⊢ 𝐵 ∈ V
Assertion	fiun	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 ⟶ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		fiun.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2		fiun.2	⊢ 𝐵 ∈ V
3		vex	⊢ 𝑢 ∈ V
4		eqeq1	⊢ ( 𝑧 = 𝑢 → ( 𝑧 = 𝐵 ↔ 𝑢 = 𝐵 ) )
5	4	rexbidv	⊢ ( 𝑧 = 𝑢 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 ) )
6	3 5	elab	⊢ ( 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 )
7		r19.29	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) )
8		nfv	⊢ Ⅎ 𝑥 Fun 𝑢
9		nfre1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵
10	9	nfab	⊢ Ⅎ 𝑥 { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 }
11		nfv	⊢ Ⅎ 𝑥 ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 )
12	10 11	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 )
13	8 12	nfan	⊢ Ⅎ 𝑥 ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )
14		ffun	⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → Fun 𝐵 )
15		funeq	⊢ ( 𝑢 = 𝐵 → ( Fun 𝑢 ↔ Fun 𝐵 ) )
16		bianir	⊢ ( ( Fun 𝐵 ∧ ( Fun 𝑢 ↔ Fun 𝐵 ) ) → Fun 𝑢 )
17	14 15 16	syl2an	⊢ ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ 𝑢 = 𝐵 ) → Fun 𝑢 )
18	17	adantlr	⊢ ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → Fun 𝑢 )
19	1	fiunlem	⊢ ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )
20	18 19	jca	⊢ ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
21	20	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) )
22	13 21	rexlimi	⊢ ( ∃ 𝑥 ∈ 𝐴 ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
23	7 22	syl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
24	6 23	sylan2b	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
25	24	ralrimiva	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∀ 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
26		fununi	⊢ ( ∀ 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) → Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
27	25 26	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
28	2	dfiun2	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 }
29	28	funeqi	⊢ ( Fun ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
30	27 29	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → Fun ∪ 𝑥 ∈ 𝐴 𝐵 )
31	3	eldm2	⊢ ( 𝑢 ∈ dom 𝐵 ↔ ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
32		fdm	⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → dom 𝐵 = 𝐷 )
33	32	eleq2d	⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → ( 𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷 ) )
34	31 33	bitr3id	⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → ( ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷 ) )
35	34	adantr	⊢ ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷 ) )
36	35	ralrexbid	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 ∈ 𝐷 ) )
37		eliun	⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
38	37	exbii	⊢ ( ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑣 ∃ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
39	3	eldm2	⊢ ( 𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
40		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ ∃ 𝑣 ∃ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
41	38 39 40	3bitr4i	⊢ ( 𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
42		eliun	⊢ ( 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 ∈ 𝐷 )
43	36 41 42	3bitr4g	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( 𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ) )
44	43	eqrdv	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷 )
45		df-fn	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ( Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷 ) )
46	30 44 45	sylanbrc	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 )
47		rniun	⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
48		frn	⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → ran 𝐵 ⊆ 𝑆 )
49	48	adantr	⊢ ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ran 𝐵 ⊆ 𝑆 )
50	49	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 )
51		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 )
52	50 51	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 )
53	47 52	eqsstrid	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆 )
54		df-f	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 ⟶ 𝑆 ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆 ) )
55	46 53 54	sylanbrc	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 ⟶ 𝑆 )