Theorem acndom2 9990

Description: A set smaller than one with choice sequences of length 𝐴 also has choice sequences of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
acndom2	⊢ (𝑋 ≼ 𝑌 → (𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴))

Proof of Theorem acndom2

Dummy variables 𝑓 𝑔 ℎ 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		brdomi 8898	. 2 ⊢ (𝑋 ≼ 𝑌 → ∃𝑓 𝑓:𝑋–1-1→𝑌)
2		simplr 767	. . . . . . . 8 ⊢ (((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) → 𝑌 ∈ AC 𝐴)
3		imassrn 6024	. . . . . . . . . . 11 ⊢ (𝑓 “ (𝑔‘𝑥)) ⊆ ran 𝑓
4		simplll 773	. . . . . . . . . . . 12 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝑋–1-1→𝑌)
5		f1f 6738	. . . . . . . . . . . 12 ⊢ (𝑓:𝑋–1-1→𝑌 → 𝑓:𝑋⟶𝑌)
6		frn 6675	. . . . . . . . . . . 12 ⊢ (𝑓:𝑋⟶𝑌 → ran 𝑓 ⊆ 𝑌)
7	4, 5, 6	3syl 18	. . . . . . . . . . 11 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → ran 𝑓 ⊆ 𝑌)
8	3, 7	sstrid 3955	. . . . . . . . . 10 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ (𝑔‘𝑥)) ⊆ 𝑌)
9		elmapi 8787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴) → 𝑔:𝐴⟶(𝒫 𝑋 ∖ {∅}))
10	9	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) → 𝑔:𝐴⟶(𝒫 𝑋 ∖ {∅}))
11	10	ffvelcdmda 7035	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ (𝒫 𝑋 ∖ {∅}))
12	11	eldifad 3922	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ 𝒫 𝑋)
13	12	elpwid 4569	. . . . . . . . . . . . . 14 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ⊆ 𝑋)
14		f1dm 6742	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝑋–1-1→𝑌 → dom 𝑓 = 𝑋)
15	4, 14	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → dom 𝑓 = 𝑋)
16	13, 15	sseqtrrd 3985	. . . . . . . . . . . . 13 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ⊆ dom 𝑓)
17		sseqin2 4175	. . . . . . . . . . . . 13 ⊢ ((𝑔‘𝑥) ⊆ dom 𝑓 ↔ (dom 𝑓 ∩ (𝑔‘𝑥)) = (𝑔‘𝑥))
18	16, 17	sylib 217	. . . . . . . . . . . 12 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (dom 𝑓 ∩ (𝑔‘𝑥)) = (𝑔‘𝑥))
19		eldifsni 4750	. . . . . . . . . . . . 13 ⊢ ((𝑔‘𝑥) ∈ (𝒫 𝑋 ∖ {∅}) → (𝑔‘𝑥) ≠ ∅)
20	11, 19	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≠ ∅)
21	18, 20	eqnetrd 3011	. . . . . . . . . . 11 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (dom 𝑓 ∩ (𝑔‘𝑥)) ≠ ∅)
22		imadisj 6032	. . . . . . . . . . . 12 ⊢ ((𝑓 “ (𝑔‘𝑥)) = ∅ ↔ (dom 𝑓 ∩ (𝑔‘𝑥)) = ∅)
23	22	necon3bii 2996	. . . . . . . . . . 11 ⊢ ((𝑓 “ (𝑔‘𝑥)) ≠ ∅ ↔ (dom 𝑓 ∩ (𝑔‘𝑥)) ≠ ∅)
24	21, 23	sylibr 233	. . . . . . . . . 10 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ (𝑔‘𝑥)) ≠ ∅)
25	8, 24	jca 512	. . . . . . . . 9 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑓 “ (𝑔‘𝑥)) ⊆ 𝑌 ∧ (𝑓 “ (𝑔‘𝑥)) ≠ ∅))
26	25	ralrimiva 3143	. . . . . . . 8 ⊢ (((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) → ∀𝑥 ∈ 𝐴 ((𝑓 “ (𝑔‘𝑥)) ⊆ 𝑌 ∧ (𝑓 “ (𝑔‘𝑥)) ≠ ∅))
27		acni2 9982	. . . . . . . 8 ⊢ ((𝑌 ∈ AC 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝑓 “ (𝑔‘𝑥)) ⊆ 𝑌 ∧ (𝑓 “ (𝑔‘𝑥)) ≠ ∅)) → ∃𝑘(𝑘:𝐴⟶𝑌 ∧ ∀𝑥 ∈ 𝐴 (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥))))
28	2, 26, 27	syl2anc 584	. . . . . . 7 ⊢ (((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) → ∃𝑘(𝑘:𝐴⟶𝑌 ∧ ∀𝑥 ∈ 𝐴 (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥))))
29		acnrcl 9978	. . . . . . . . 9 ⊢ (𝑌 ∈ AC 𝐴 → 𝐴 ∈ V)
30	29	ad3antlr 729	. . . . . . . 8 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ (𝑘:𝐴⟶𝑌 ∧ ∀𝑥 ∈ 𝐴 (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → 𝐴 ∈ V)
31		simp-4l 781	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → 𝑓:𝑋–1-1→𝑌)
32		f1f1orn 6795	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝑋–1-1→𝑌 → 𝑓:𝑋–1-1-onto→ran 𝑓)
33	31, 32	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → 𝑓:𝑋–1-1-onto→ran 𝑓)
34		simprr 771	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))
35	3, 34	sselid 3942	. . . . . . . . . . . . . 14 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → (𝑘‘𝑥) ∈ ran 𝑓)
36		f1ocnvfv2 7223	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝑋–1-1-onto→ran 𝑓 ∧ (𝑘‘𝑥) ∈ ran 𝑓) → (𝑓‘(◡𝑓‘(𝑘‘𝑥))) = (𝑘‘𝑥))
37	33, 35, 36	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → (𝑓‘(◡𝑓‘(𝑘‘𝑥))) = (𝑘‘𝑥))
38	37, 34	eqeltrd 2838	. . . . . . . . . . . 12 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → (𝑓‘(◡𝑓‘(𝑘‘𝑥))) ∈ (𝑓 “ (𝑔‘𝑥)))
39		f1ocnv 6796	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝑋–1-1-onto→ran 𝑓 → ◡𝑓:ran 𝑓–1-1-onto→𝑋)
40		f1of 6784	. . . . . . . . . . . . . . 15 ⊢ (◡𝑓:ran 𝑓–1-1-onto→𝑋 → ◡𝑓:ran 𝑓⟶𝑋)
41	33, 39, 40	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → ◡𝑓:ran 𝑓⟶𝑋)
42	41, 35	ffvelcdmd 7036	. . . . . . . . . . . . 13 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → (◡𝑓‘(𝑘‘𝑥)) ∈ 𝑋)
43	13	ad2ant2r 745	. . . . . . . . . . . . 13 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → (𝑔‘𝑥) ⊆ 𝑋)
44		f1elima 7210	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑋–1-1→𝑌 ∧ (◡𝑓‘(𝑘‘𝑥)) ∈ 𝑋 ∧ (𝑔‘𝑥) ⊆ 𝑋) → ((𝑓‘(◡𝑓‘(𝑘‘𝑥))) ∈ (𝑓 “ (𝑔‘𝑥)) ↔ (◡𝑓‘(𝑘‘𝑥)) ∈ (𝑔‘𝑥)))
45	31, 42, 43, 44	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → ((𝑓‘(◡𝑓‘(𝑘‘𝑥))) ∈ (𝑓 “ (𝑔‘𝑥)) ↔ (◡𝑓‘(𝑘‘𝑥)) ∈ (𝑔‘𝑥)))
46	38, 45	mpbid 231	. . . . . . . . . . 11 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ (𝑥 ∈ 𝐴 ∧ (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → (◡𝑓‘(𝑘‘𝑥)) ∈ (𝑔‘𝑥))
47	46	expr 457	. . . . . . . . . 10 ⊢ (((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) ∧ 𝑥 ∈ 𝐴) → ((𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)) → (◡𝑓‘(𝑘‘𝑥)) ∈ (𝑔‘𝑥)))
48	47	ralimdva 3164	. . . . . . . . 9 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ 𝑘:𝐴⟶𝑌) → (∀𝑥 ∈ 𝐴 (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)) → ∀𝑥 ∈ 𝐴 (◡𝑓‘(𝑘‘𝑥)) ∈ (𝑔‘𝑥)))
49	48	impr 455	. . . . . . . 8 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ (𝑘:𝐴⟶𝑌 ∧ ∀𝑥 ∈ 𝐴 (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → ∀𝑥 ∈ 𝐴 (◡𝑓‘(𝑘‘𝑥)) ∈ (𝑔‘𝑥))
50		acnlem 9984	. . . . . . . 8 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 (◡𝑓‘(𝑘‘𝑥)) ∈ (𝑔‘𝑥)) → ∃ℎ∀𝑥 ∈ 𝐴 (ℎ‘𝑥) ∈ (𝑔‘𝑥))
51	30, 49, 50	syl2anc 584	. . . . . . 7 ⊢ ((((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) ∧ (𝑘:𝐴⟶𝑌 ∧ ∀𝑥 ∈ 𝐴 (𝑘‘𝑥) ∈ (𝑓 “ (𝑔‘𝑥)))) → ∃ℎ∀𝑥 ∈ 𝐴 (ℎ‘𝑥) ∈ (𝑔‘𝑥))
52	28, 51	exlimddv 1938	. . . . . 6 ⊢ (((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)) → ∃ℎ∀𝑥 ∈ 𝐴 (ℎ‘𝑥) ∈ (𝑔‘𝑥))
53	52	ralrimiva 3143	. . . . 5 ⊢ ((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) → ∀𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)∃ℎ∀𝑥 ∈ 𝐴 (ℎ‘𝑥) ∈ (𝑔‘𝑥))
54		vex 3449	. . . . . . . 8 ⊢ 𝑓 ∈ V
55	54	dmex 7848	. . . . . . 7 ⊢ dom 𝑓 ∈ V
56	14, 55	eqeltrrdi 2847	. . . . . 6 ⊢ (𝑓:𝑋–1-1→𝑌 → 𝑋 ∈ V)
57		isacn 9980	. . . . . 6 ⊢ ((𝑋 ∈ V ∧ 𝐴 ∈ V) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)∃ℎ∀𝑥 ∈ 𝐴 (ℎ‘𝑥) ∈ (𝑔‘𝑥)))
58	56, 29, 57	syl2an 596	. . . . 5 ⊢ ((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑔 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)∃ℎ∀𝑥 ∈ 𝐴 (ℎ‘𝑥) ∈ (𝑔‘𝑥)))
59	53, 58	mpbird 256	. . . 4 ⊢ ((𝑓:𝑋–1-1→𝑌 ∧ 𝑌 ∈ AC 𝐴) → 𝑋 ∈ AC 𝐴)
60	59	ex 413	. . 3 ⊢ (𝑓:𝑋–1-1→𝑌 → (𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴))
61	60	exlimiv 1933	. 2 ⊢ (∃𝑓 𝑓:𝑋–1-1→𝑌 → (𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴))
62	1, 61	syl 17	1 ⊢ (𝑋 ≼ 𝑌 → (𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  Vcvv 3445   ∖ cdif 3907   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  𝒫 cpw 4560  {csn 4586   class class class wbr 5105  ^◡ccnv 5632  dom cdm 5633  ran crn 5634   “ cima 5636  ⟶wf 6492  –1-1→wf1 6493  –1-1-onto→wf1o 6495  ‘cfv 6496  (class class class)co 7357   ↑_m cmap 8765   ≼ cdom 8881  AC wacn 9874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767  df-dom 8885  df-acn 9878

This theorem is referenced by:  acnen2  9991  dfac13  10078  iundomg  10477  iunctb  10510