Theorem f1iun 7968

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.) (Proof shortened by AV, 5-Nov-2023.)

Hypotheses

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

Assertion

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

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

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

Proof of Theorem f1iun

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

Step	Hyp	Ref	Expression
1		vex 3484	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
2		eqeq1 2741	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝑧 = 𝐵 ↔ 𝑢 = 𝐵))
3	2	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵))
4	1, 3	elab 3679	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵)
5		r19.29 3114	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵))
6		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(Fun 𝑢 ∧ Fun ◡𝑢)
7		nfre1 3285	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵
8	7	nfab 2911	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
9		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
10	8, 9	nfralw 3311	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
11	6, 10	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
12		f1eq1 6799	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝐵 → (𝑢:𝐷–1-1→𝑆 ↔ 𝐵:𝐷–1-1→𝑆))
13	12	biimparc 479	. . . . . . . . . . . . . . 15 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → 𝑢:𝐷–1-1→𝑆)
14		df-f1 6566	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:𝐷–1-1→𝑆 ↔ (𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢))
15		ffun 6739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢:𝐷⟶𝑆 → Fun 𝑢)
16	15	anim1i 615	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢) → (Fun 𝑢 ∧ Fun ◡𝑢))
17	14, 16	sylbi 217	. . . . . . . . . . . . . . 15 ⊢ (𝑢:𝐷–1-1→𝑆 → (Fun 𝑢 ∧ Fun ◡𝑢))
18	13, 17	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢))
19	18	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢))
20		f1f 6804	. . . . . . . . . . . . . 14 ⊢ (𝐵:𝐷–1-1→𝑆 → 𝐵:𝐷⟶𝑆)
21		fiun.1	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
22	21	fiunlem 7966	. . . . . . . . . . . . . 14 ⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
23	20, 22	sylanl1 680	. . . . . . . . . . . . 13 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
24	19, 23	jca 511	. . . . . . . . . . . 12 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
25	24	a1i 11	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
26	11, 25	rexlimi 3259	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
27	5, 26	syl 17	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
28	4, 27	sylan2b 594	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
29	28	ralrimiva 3146	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
30		fun11uni 7955	. . . . . . 7 ⊢ (∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → (Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}))
31	29, 30	syl 17	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}))
32	31	simpld 494	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
33		fiun.2	. . . . . . 7 ⊢ 𝐵 ∈ V
34	33	dfiun2 5033	. . . . . 6 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
35	34	funeqi 6587	. . . . 5 ⊢ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
36	32, 35	sylibr 234	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ 𝑥 ∈ 𝐴 𝐵)
37	1	eldm2 5912	. . . . . . . . 9 ⊢ (𝑢 ∈ dom 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
38		f1dm 6808	. . . . . . . . . 10 ⊢ (𝐵:𝐷–1-1→𝑆 → dom 𝐵 = 𝐷)
39	38	eleq2d 2827	. . . . . . . . 9 ⊢ (𝐵:𝐷–1-1→𝑆 → (𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷))
40	37, 39	bitr3id 285	. . . . . . . 8 ⊢ (𝐵:𝐷–1-1→𝑆 → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
41	40	adantr 480	. . . . . . 7 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
42	41	ralrexbid 3106	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷))
43		eliun 4995	. . . . . . . 8 ⊢ (⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
44	43	exbii 1848	. . . . . . 7 ⊢ (∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
45	1	eldm2 5912	. . . . . . 7 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
46		rexcom4 3288	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
47	44, 45, 46	3bitr4i 303	. . . . . 6 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
48		eliun 4995	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷)
49	42, 47, 48	3bitr4g 314	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷))
50	49	eqrdv 2735	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷)
51		df-fn 6564	. . . 4 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ↔ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷))
52	36, 50, 51	sylanbrc 583	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷)
53		rniun 6167	. . . 4 ⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
54	20	frnd 6744	. . . . . . 7 ⊢ (𝐵:𝐷–1-1→𝑆 → ran 𝐵 ⊆ 𝑆)
55	54	adantr 480	. . . . . 6 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran 𝐵 ⊆ 𝑆)
56	55	ralimi 3083	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
57		iunss 5045	. . . . 5 ⊢ (∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
58	56, 57	sylibr 234	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
59	53, 58	eqsstrid 4022	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆)
60		df-f 6565	. . 3 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆))
61	52, 59, 60	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆)
62	31	simprd 495	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
63	34	cnveqi 5885	. . . 4 ⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
64	63	funeqi 6587	. . 3 ⊢ (Fun ◡∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
65	62, 64	sylibr 234	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ 𝑥 ∈ 𝐴 𝐵)
66		df-f1 6566	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ∧ Fun ◡∪ 𝑥 ∈ 𝐴 𝐵))
67	61, 65, 66	sylanbrc 583	1 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1540  ∃wex 1779   ∈ wcel 2108  {cab 2714  ∀wral 3061  ∃wrex 3070  Vcvv 3480   ⊆ wss 3951  ⟨cop 4632  ∪ cuni 4907  ∪ ciun 4991  ^◡ccnv 5684  dom cdm 5685  ran crn 5686  Fun wfun 6555   Fn wfn 6556  ⟶wf 6557  –1-1→wf1 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566

This theorem is referenced by:  ackbij2  10282