Theorem f1iun 7950

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 3467	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
2		eqeq1 2738	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝑧 = 𝐵 ↔ 𝑢 = 𝐵))
3	2	rexbidv 3166	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵))
4	1, 3	elab 3662	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵)
5		r19.29 3101	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵))
6		nfv 1913	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(Fun 𝑢 ∧ Fun ◡𝑢)
7		nfre1 3270	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵
8	7	nfab 2903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
9		nfv 1913	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
10	8, 9	nfralw 3294	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
11	6, 10	nfan 1898	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
12		f1eq1 6779	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝐵 → (𝑢:𝐷–1-1→𝑆 ↔ 𝐵:𝐷–1-1→𝑆))
13	12	biimparc 479	. . . . . . . . . . . . . . 15 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → 𝑢:𝐷–1-1→𝑆)
14		df-f1 6546	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:𝐷–1-1→𝑆 ↔ (𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢))
15		ffun 6719	. . . . . . . . . . . . . . . . 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 6784	. . . . . . . . . . . . . 14 ⊢ (𝐵:𝐷–1-1→𝑆 → 𝐵:𝐷⟶𝑆)
21		fiun.1	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
22	21	fiunlem 7948	. . . . . . . . . . . . . 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 3245	. . . . . . . . . 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 3133	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
30		fun11uni 7937	. . . . . . 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 5013	. . . . . 6 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
35	34	funeqi 6567	. . . . 5 ⊢ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
36	32, 35	sylibr 234	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ 𝑥 ∈ 𝐴 𝐵)
37	1	eldm2 5892	. . . . . . . . 9 ⊢ (𝑢 ∈ dom 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
38		f1dm 6788	. . . . . . . . . 10 ⊢ (𝐵:𝐷–1-1→𝑆 → dom 𝐵 = 𝐷)
39	38	eleq2d 2819	. . . . . . . . 9 ⊢ (𝐵:𝐷–1-1→𝑆 → (𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷))
40	37, 39	bitr3id 285	. . . . . . . 8 ⊢ (𝐵:𝐷–1-1→𝑆 → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
41	40	adantr 480	. . . . . . 7 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
42	41	ralrexbid 3093	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷))
43		eliun 4975	. . . . . . . 8 ⊢ (⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
44	43	exbii 1847	. . . . . . 7 ⊢ (∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
45	1	eldm2 5892	. . . . . . 7 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
46		rexcom4 3272	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
47	44, 45, 46	3bitr4i 303	. . . . . 6 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
48		eliun 4975	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷)
49	42, 47, 48	3bitr4g 314	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷))
50	49	eqrdv 2732	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷)
51		df-fn 6544	. . . 4 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ↔ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷))
52	36, 50, 51	sylanbrc 583	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷)
53		rniun 6147	. . . 4 ⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
54	20	frnd 6724	. . . . . . 7 ⊢ (𝐵:𝐷–1-1→𝑆 → ran 𝐵 ⊆ 𝑆)
55	54	adantr 480	. . . . . 6 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran 𝐵 ⊆ 𝑆)
56	55	ralimi 3072	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
57		iunss 5025	. . . . 5 ⊢ (∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
58	56, 57	sylibr 234	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
59	53, 58	eqsstrid 4002	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆)
60		df-f 6545	. . 3 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆))
61	52, 59, 60	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆)
62	31	simprd 495	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
63	34	cnveqi 5865	. . . 4 ⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
64	63	funeqi 6567	. . 3 ⊢ (Fun ◡∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
65	62, 64	sylibr 234	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ 𝑥 ∈ 𝐴 𝐵)
66		df-f1 6546	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ∧ Fun ◡∪ 𝑥 ∈ 𝐴 𝐵))
67	61, 65, 66	sylanbrc 583	1 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1539  ∃wex 1778   ∈ wcel 2107  {cab 2712  ∀wral 3050  ∃wrex 3059  Vcvv 3463   ⊆ wss 3931  ⟨cop 4612  ∪ cuni 4887  ∪ ciun 4971  ^◡ccnv 5664  dom cdm 5665  ran crn 5666  Fun wfun 6535   Fn wfn 6536  ⟶wf 6537  –1-1→wf1 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546

This theorem is referenced by:  ackbij2  10264