Theorem f1iun 7645

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 3497	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
2		eqeq1 2825	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝑧 = 𝐵 ↔ 𝑢 = 𝐵))
3	2	rexbidv 3297	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵))
4	1, 3	elab 3667	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵)
5		r19.29 3254	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵))
6		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(Fun 𝑢 ∧ Fun ◡𝑢)
7		nfre1 3306	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵
8	7	nfab 2984	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
9		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
10	8, 9	nfralw 3225	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)
11	6, 10	nfan 1900	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
12		f1eq1 6570	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝐵 → (𝑢:𝐷–1-1→𝑆 ↔ 𝐵:𝐷–1-1→𝑆))
13	12	biimparc 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → 𝑢:𝐷–1-1→𝑆)
14		df-f1 6360	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:𝐷–1-1→𝑆 ↔ (𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢))
15		ffun 6517	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢:𝐷⟶𝑆 → Fun 𝑢)
16	15	anim1i 616	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢) → (Fun 𝑢 ∧ Fun ◡𝑢))
17	14, 16	sylbi 219	. . . . . . . . . . . . . . 15 ⊢ (𝑢:𝐷–1-1→𝑆 → (Fun 𝑢 ∧ Fun ◡𝑢))
18	13, 17	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢))
19	18	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢))
20		f1f 6575	. . . . . . . . . . . . . 14 ⊢ (𝐵:𝐷–1-1→𝑆 → 𝐵:𝐷⟶𝑆)
21		fiun.1	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
22	21	fiunlem 7643	. . . . . . . . . . . . . 14 ⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
23	20, 22	sylanl1 678	. . . . . . . . . . . . 13 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
24	19, 23	jca 514	. . . . . . . . . . . 12 ⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
25	24	a1i 11	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
26	11, 25	rexlimi 3315	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
27	5, 26	syl 17	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
28	4, 27	sylan2b 595	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
29	28	ralrimiva 3182	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
30		fun11uni 7637	. . . . . . 7 ⊢ (∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → (Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}))
31	29, 30	syl 17	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}))
32	31	simpld 497	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
33		fiun.2	. . . . . . 7 ⊢ 𝐵 ∈ V
34	33	dfiun2 4958	. . . . . 6 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
35	34	funeqi 6376	. . . . 5 ⊢ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
36	32, 35	sylibr 236	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ 𝑥 ∈ 𝐴 𝐵)
37	1	eldm2 5770	. . . . . . . . 9 ⊢ (𝑢 ∈ dom 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
38		f1dm 6579	. . . . . . . . . 10 ⊢ (𝐵:𝐷–1-1→𝑆 → dom 𝐵 = 𝐷)
39	38	eleq2d 2898	. . . . . . . . 9 ⊢ (𝐵:𝐷–1-1→𝑆 → (𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷))
40	37, 39	syl5bbr 287	. . . . . . . 8 ⊢ (𝐵:𝐷–1-1→𝑆 → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
41	40	adantr 483	. . . . . . 7 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷))
42	41	ralrexbid 3322	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷))
43		eliun 4923	. . . . . . . 8 ⊢ (⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
44	43	exbii 1848	. . . . . . 7 ⊢ (∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
45	1	eldm2 5770	. . . . . . 7 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
46		rexcom4 3249	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵)
47	44, 45, 46	3bitr4i 305	. . . . . 6 ⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵)
48		eliun 4923	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷)
49	42, 47, 48	3bitr4g 316	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷))
50	49	eqrdv 2819	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷)
51		df-fn 6358	. . . 4 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ↔ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷))
52	36, 50, 51	sylanbrc 585	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷)
53		rniun 6006	. . . 4 ⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
54	20	frnd 6521	. . . . . . 7 ⊢ (𝐵:𝐷–1-1→𝑆 → ran 𝐵 ⊆ 𝑆)
55	54	adantr 483	. . . . . 6 ⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran 𝐵 ⊆ 𝑆)
56	55	ralimi 3160	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
57		iunss 4969	. . . . 5 ⊢ (∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
58	56, 57	sylibr 236	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆)
59	53, 58	eqsstrid 4015	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆)
60		df-f 6359	. . 3 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆))
61	52, 59, 60	sylanbrc 585	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆)
62	31	simprd 498	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
63	34	cnveqi 5745	. . . 4 ⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}
64	63	funeqi 6376	. . 3 ⊢ (Fun ◡∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})
65	62, 64	sylibr 236	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ 𝑥 ∈ 𝐴 𝐵)
66		df-f1 6360	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆 ↔ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ∧ Fun ◡∪ 𝑥 ∈ 𝐴 𝐵))
67	61, 65, 66	sylanbrc 585	1 ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2799  ∀wral 3138  ∃wrex 3139  Vcvv 3494   ⊆ wss 3936  ⟨cop 4573  ∪ cuni 4838  ∪ ciun 4919  ^◡ccnv 5554  dom cdm 5555  ran crn 5556  Fun wfun 6349   Fn wfn 6350  ⟶wf 6351  –1-1→wf1 6352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360

This theorem is referenced by:  ackbij2  9665