ackbij1lem16 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ackbij1lem16		Structured version Visualization version GIF version

Theorem ackbij1lem16 10191

Description: Lemma for ackbij1 10194. (Contributed by Stefan O'Rear, 18-Nov-2014.)

**Hypothesis**
Ref	Expression
ackbij.f	⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))

**Assertion**
Ref	Expression
ackbij1lem16	⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))

Distinct variable groups: 𝑥,𝐹,𝑦 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦

Proof of Theorem ackbij1lem16 Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 4189	. . . . . . . . 9 ⊢ (𝒫 ω ∩ Fin) ⊆ 𝒫 ω
2	1	sseli 3933	. . . . . . . 8 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ 𝒫 ω)
3	2	elpwid 4565	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ⊆ ω)
4	3	adantr 484	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ ω)
5	1	sseli 3933	. . . . . . . 8 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ 𝒫 ω)
6	5	elpwid 4565	. . . . . . 7 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ⊆ ω)
7	6	adantl 485	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ ω)
8	4, 7	unssd 4145	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ ω)
9		inss2 4190	. . . . . . 7 ⊢ (𝒫 ω ∩ Fin) ⊆ Fin
10	9	sseli 3933	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ Fin)
11	9	sseli 3933	. . . . . 6 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ Fin)
12		unfi 9140	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
13	10, 11, 12	syl2an 605	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ Fin)
14		nnunifi 9236	. . . . 5 ⊢ (((𝐴 ∪ 𝐵) ⊆ ω ∧ (𝐴 ∪ 𝐵) ∈ Fin) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
15	8, 13, 14	syl2anc 593	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
16		peano2 7871	. . . 4 ⊢ (∪ (𝐴 ∪ 𝐵) ∈ ω → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
17	15, 16	syl 17	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
18		ineq2 4167	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐴 ∩ 𝑎) = (𝐴 ∩ ∅))
19	18	fveq2d 6872	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ ∅)))
20		ineq2 4167	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐵 ∩ 𝑎) = (𝐵 ∩ ∅))
21	20	fveq2d 6872	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ ∅)))
22	19, 21	eqeq12d 2779	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅))))
23	18, 20	eqeq12d 2779	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
24	22, 23	imbi12d 346	. . . . 5 ⊢ (𝑎 = ∅ → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅))))
25	24	imbi2d 342	. . . 4 ⊢ (𝑎 = ∅ → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))))
26		ineq2 4167	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ 𝑏))
27	26	fveq2d 6872	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ 𝑏)))
28		ineq2 4167	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ 𝑏))
29	28	fveq2d 6872	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑏)))
30	27, 29	eqeq12d 2779	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
31	26, 28	eqeq12d 2779	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
32	30, 31	imbi12d 346	. . . . 5 ⊢ (𝑎 = 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏))))
33	32	imbi2d 342	. . . 4 ⊢ (𝑎 = 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))))
34		ineq2 4167	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc 𝑏))
35	34	fveq2d 6872	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
36		ineq2 4167	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc 𝑏))
37	36	fveq2d 6872	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
38	35, 37	eqeq12d 2779	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))))
39	34, 36	eqeq12d 2779	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
40	38, 39	imbi12d 346	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
41	40	imbi2d 342	. . . 4 ⊢ (𝑎 = suc 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
42		ineq2 4167	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)))
43	42	fveq2d 6872	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))))
44		ineq2 4167	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))
45	44	fveq2d 6872	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
46	43, 45	eqeq12d 2779	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
47	42, 44	eqeq12d 2779	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
48	46, 47	imbi12d 346	. . . . 5 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
49	48	imbi2d 342	. . . 4 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))))
50		in0 4350	. . . . . 6 ⊢ (𝐴 ∩ ∅) = ∅
51		in0 4350	. . . . . 6 ⊢ (𝐵 ∩ ∅) = ∅
52	50, 51	eqtr4i 2789	. . . . 5 ⊢ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)
53	52	2a1i 12	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
54		simp13 1220	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
55		3simpa 1162	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))))
56		ackbij1lem2 10177	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
57	56	fveq2d 6872	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐴 → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
58	57	3ad2ant2 1148	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
59		ackbij1lem4 10179	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ω → {𝑏} ∈ (𝒫 ω ∩ Fin))
60	59	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → {𝑏} ∈ (𝒫 ω ∩ Fin))
61		simprl 780	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐴 ∈ (𝒫 ω ∩ Fin))
62		inss1 4189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝐴
63		ackbij.f	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
64	63	ackbij1lem11 10186	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ⊆ 𝐴) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
65	61, 62, 64	sylancl 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
66		incom 4162	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ((𝐴 ∩ 𝑏) ∩ {𝑏})
67		inss2 4190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝑏
68		nnord 7855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ ω → Ord 𝑏)
69		orddisj 6385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord 𝑏 → (𝑏 ∩ {𝑏}) = ∅)
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ ω → (𝑏 ∩ {𝑏}) = ∅)
71	70	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝑏 ∩ {𝑏}) = ∅)
72		ssdisj 4415	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
73	67, 71, 72	sylancr 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
74	66, 73	eqtrid 2810	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅)
75	63	ackbij1lem9 10184	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
76	60, 65, 74, 75	syl3anc 1391	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
77	76	3ad2ant1 1147	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
78	58, 77	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
79	55, 78	syl3an1 1177	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
80		ackbij1lem2 10177	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
81	80	fveq2d 6872	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐵 → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
82	81	3ad2ant3 1149	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
83		simprr 782	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐵 ∈ (𝒫 ω ∩ Fin))
84		inss1 4189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝐵
85	63	ackbij1lem11 10186	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ⊆ 𝐵) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
86	83, 84, 85	sylancl 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
87		incom 4162	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ((𝐵 ∩ 𝑏) ∩ {𝑏})
88		inss2 4190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝑏
89		ssdisj 4415	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
90	88, 71, 89	sylancr 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
91	87, 90	eqtrid 2810	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅)
92	63	ackbij1lem9 10184	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
93	60, 86, 91, 92	syl3anc 1391	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
94	93	3ad2ant1 1147	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
95	82, 94	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
96	55, 95	syl3an1 1177	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
97	54, 79, 96	3eqtr3d 2806	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
98	63	ackbij1lem10 10185	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
99	98	ffvelcdmi 7065	. . . . . . . . . . . . . . . 16 ⊢ ({𝑏} ∈ (𝒫 ω ∩ Fin) → (𝐹‘{𝑏}) ∈ ω)
100	60, 99	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘{𝑏}) ∈ ω)
101	98	ffvelcdmi 7065	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
102	65, 101	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
103	98	ffvelcdmi 7065	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
104	86, 103	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
105		nnacan 8599	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘{𝑏}) ∈ ω ∧ (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω ∧ (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
106	100, 102, 104, 105	syl3anc 1391	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
107	106	3adant3 1146	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
108	107	3ad2ant1 1147	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
109	97, 108	mpbid 234	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
110		uneq2 4116	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
111	110	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
112	56	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
113	80	ad2antlr 737	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
114	111, 112, 113	3eqtr4d 2808	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))
115	114	ex 416	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
116	115	3adant1 1144	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
117	109, 116	embantd 59	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
118	117	3exp 1133	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
119		simp13 1220	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
120	119	eqcomd 2769	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
121		simp12r 1302	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
122		simp12l 1301	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
123		simp11 1218	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
124		simp3 1152	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
125		simp2 1151	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐴)
126	63	ackbij1lem15 10190	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐵 ∧ ¬ 𝑏 ∈ 𝐴)) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
127	121, 122, 123, 124, 125, 126	syl23anc 1397	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
128	120, 127	pm2.21dd 197	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
129	128	3exp 1133	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
130	118, 129	pm2.61d 180	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
131		simp13 1220	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
132		simp12l 1301	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
133		simp12r 1302	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
134		simp11 1218	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
135		simp2 1151	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
136		simp3 1152	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐵)
137	63	ackbij1lem15 10190	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
138	132, 133, 134, 135, 136, 137	syl23anc 1397	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
139	131, 138	pm2.21dd 197	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
140	139	3exp 1133	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
141		simp13 1220	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
142		ackbij1lem1 10176	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
143	142	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
144	143	fveq2d 6872	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ 𝑏)))
145		ackbij1lem1 10176	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
146	145	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
147	146	fveq2d 6872	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
148	144, 147	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
149	148	biimpd 231	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
150	149	3adant1 1144	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
151	141, 150	mpd 15	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
152	143, 146	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
153	152	biimprd 250	. . . . . . . . . . . 12 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
154	153	3adant1 1144	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
155	151, 154	embantd 59	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
156	155	3exp 1133	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
157	140, 156	pm2.61d 180	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
158	130, 157	pm2.61d 180	. . . . . . 7 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
159	158	3exp 1133	. . . . . 6 ⊢ (𝑏 ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
160	159	com34 91	. . . . 5 ⊢ (𝑏 ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
161	160	a2d 29	. . . 4 ⊢ (𝑏 ∈ ω → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏))) → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
162	25, 33, 41, 49, 53, 161	finds 7878	. . 3 ⊢ (suc ∪ (𝐴 ∪ 𝐵) ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
163	17, 162	mpcom 38	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
164		omsson 7851	. . . . . . . 8 ⊢ ω ⊆ On
165	8, 164	sstrdi 3949	. . . . . . 7 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ On)
166		onsucuni 7809	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ⊆ On → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
167	165, 166	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
168	167	unssad 4146	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵))
169		dfss2 3923	. . . . 5 ⊢ (𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
170	168, 169	sylib 220	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
171	170	fveq2d 6872	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐴))
172	167	unssbd 4147	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵))
173		dfss2 3923	. . . . 5 ⊢ (𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
174	172, 173	sylib 220	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
175	174	fveq2d 6872	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐵))
176	171, 175	eqeq12d 2779	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) ↔ (𝐹‘𝐴) = (𝐹‘𝐵)))
177	170, 174	eqeq12d 2779	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) ↔ 𝐴 = 𝐵))
178	163, 176, 177	3imtr3d 295	1 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1099 = wceq 1561 ∈ wcel 2143 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 𝒫 cpw 4556 {csn 4583 ∪ cuni 4866 ∪ ciun 4950 ↦ cmpt 5182 × cxp 5646 Ord word 6346 Oncon0 6347 suc csuc 6349 ‘cfv 6522 (class class class)co 7397 ωcom 7847 +_o coa 8435 Fincfn 8928 cardccrd 9894

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1816 ax-4 1830 ax-5 1931 ax-6 1988 ax-7 2029 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5247 ax-nul 5257 ax-pow 5323 ax-pr 5391 ax-un 7719

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1564 df-fal 1574 df-ex 1801 df-nf 1805 df-sb 2092 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3078 df-rex 3088 df-reu 3369 df-rab 3416 df-v 3457 df-sbc 3746 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5102 df-opab 5164 df-mpt 5183 df-tr 5209 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6289 df-ord 6350 df-on 6351 df-lim 6352 df-suc 6353 df-iota 6478 df-fun 6524 df-fn 6525 df-f 6526 df-f1 6527 df-fo 6528 df-f1o 6529 df-fv 6530 df-ov 7400 df-oprab 7401 df-mpo 7402 df-om 7848 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8382 df-1o 8438 df-2o 8439 df-oadd 8442 df-er 8679 df-map 8811 df-en 8929 df-dom 8930 df-sdom 8931 df-fin 8932 df-dju 9860 df-card 9898

This theorem is referenced by: ackbij1lem17 10192

W3C validator