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 9991

Description: Lemma for ackbij1 9994. (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 4162	. . . . . . . . 9 ⊢ (𝒫 ω ∩ Fin) ⊆ 𝒫 ω
2	1	sseli 3917	. . . . . . . 8 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ 𝒫 ω)
3	2	elpwid 4544	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ⊆ ω)
4	3	adantr 481	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ ω)
5	1	sseli 3917	. . . . . . . 8 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ 𝒫 ω)
6	5	elpwid 4544	. . . . . . 7 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ⊆ ω)
7	6	adantl 482	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ ω)
8	4, 7	unssd 4120	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ ω)
9		inss2 4163	. . . . . . 7 ⊢ (𝒫 ω ∩ Fin) ⊆ Fin
10	9	sseli 3917	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ Fin)
11	9	sseli 3917	. . . . . 6 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ Fin)
12		unfi 8955	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
13	10, 11, 12	syl2an 596	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ Fin)
14		nnunifi 9065	. . . . 5 ⊢ (((𝐴 ∪ 𝐵) ⊆ ω ∧ (𝐴 ∪ 𝐵) ∈ Fin) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
15	8, 13, 14	syl2anc 584	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
16		peano2 7737	. . . 4 ⊢ (∪ (𝐴 ∪ 𝐵) ∈ ω → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
17	15, 16	syl 17	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
18		ineq2 4140	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐴 ∩ 𝑎) = (𝐴 ∩ ∅))
19	18	fveq2d 6778	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ ∅)))
20		ineq2 4140	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐵 ∩ 𝑎) = (𝐵 ∩ ∅))
21	20	fveq2d 6778	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ ∅)))
22	19, 21	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅))))
23	18, 20	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
24	22, 23	imbi12d 345	. . . . 5 ⊢ (𝑎 = ∅ → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅))))
25	24	imbi2d 341	. . . 4 ⊢ (𝑎 = ∅ → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))))
26		ineq2 4140	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ 𝑏))
27	26	fveq2d 6778	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ 𝑏)))
28		ineq2 4140	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ 𝑏))
29	28	fveq2d 6778	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑏)))
30	27, 29	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
31	26, 28	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
32	30, 31	imbi12d 345	. . . . 5 ⊢ (𝑎 = 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏))))
33	32	imbi2d 341	. . . 4 ⊢ (𝑎 = 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))))
34		ineq2 4140	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc 𝑏))
35	34	fveq2d 6778	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
36		ineq2 4140	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc 𝑏))
37	36	fveq2d 6778	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
38	35, 37	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))))
39	34, 36	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
40	38, 39	imbi12d 345	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
41	40	imbi2d 341	. . . 4 ⊢ (𝑎 = suc 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
42		ineq2 4140	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)))
43	42	fveq2d 6778	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))))
44		ineq2 4140	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))
45	44	fveq2d 6778	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
46	43, 45	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
47	42, 44	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
48	46, 47	imbi12d 345	. . . . 5 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
49	48	imbi2d 341	. . . 4 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))))
50		in0 4325	. . . . . 6 ⊢ (𝐴 ∩ ∅) = ∅
51		in0 4325	. . . . . 6 ⊢ (𝐵 ∩ ∅) = ∅
52	50, 51	eqtr4i 2769	. . . . 5 ⊢ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)
53	52	2a1i 12	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
54		simp13 1204	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
55		3simpa 1147	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))))
56		ackbij1lem2 9977	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
57	56	fveq2d 6778	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐴 → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
58	57	3ad2ant2 1133	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
59		ackbij1lem4 9979	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ω → {𝑏} ∈ (𝒫 ω ∩ Fin))
60	59	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → {𝑏} ∈ (𝒫 ω ∩ Fin))
61		simprl 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐴 ∈ (𝒫 ω ∩ Fin))
62		inss1 4162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝐴
63		ackbij.f	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
64	63	ackbij1lem11 9986	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ⊆ 𝐴) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
65	61, 62, 64	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
66		incom 4135	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ((𝐴 ∩ 𝑏) ∩ {𝑏})
67		inss2 4163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝑏
68		nnord 7720	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ ω → Ord 𝑏)
69		orddisj 6304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord 𝑏 → (𝑏 ∩ {𝑏}) = ∅)
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ ω → (𝑏 ∩ {𝑏}) = ∅)
71	70	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝑏 ∩ {𝑏}) = ∅)
72		ssdisj 4393	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
73	67, 71, 72	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
74	66, 73	eqtrid 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅)
75	63	ackbij1lem9 9984	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
76	60, 65, 74, 75	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
77	76	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
78	58, 77	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
79	55, 78	syl3an1 1162	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
80		ackbij1lem2 9977	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
81	80	fveq2d 6778	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐵 → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
82	81	3ad2ant3 1134	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
83		simprr 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐵 ∈ (𝒫 ω ∩ Fin))
84		inss1 4162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝐵
85	63	ackbij1lem11 9986	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ⊆ 𝐵) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
86	83, 84, 85	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
87		incom 4135	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ((𝐵 ∩ 𝑏) ∩ {𝑏})
88		inss2 4163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝑏
89		ssdisj 4393	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
90	88, 71, 89	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
91	87, 90	eqtrid 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅)
92	63	ackbij1lem9 9984	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
93	60, 86, 91, 92	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
94	93	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
95	82, 94	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
96	55, 95	syl3an1 1162	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
97	54, 79, 96	3eqtr3d 2786	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
98	63	ackbij1lem10 9985	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
99	98	ffvelrni 6960	. . . . . . . . . . . . . . . 16 ⊢ ({𝑏} ∈ (𝒫 ω ∩ Fin) → (𝐹‘{𝑏}) ∈ ω)
100	60, 99	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘{𝑏}) ∈ ω)
101	98	ffvelrni 6960	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
102	65, 101	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
103	98	ffvelrni 6960	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
104	86, 103	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
105		nnacan 8459	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘{𝑏}) ∈ ω ∧ (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω ∧ (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
106	100, 102, 104, 105	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
107	106	3adant3 1131	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
108	107	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
109	97, 108	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
110		uneq2 4091	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
111	110	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
112	56	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
113	80	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
114	111, 112, 113	3eqtr4d 2788	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))
115	114	ex 413	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
116	115	3adant1 1129	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
117	109, 116	embantd 59	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
118	117	3exp 1118	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
119		simp13 1204	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
120	119	eqcomd 2744	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
121		simp12r 1286	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
122		simp12l 1285	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
123		simp11 1202	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
124		simp3 1137	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
125		simp2 1136	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐴)
126	63	ackbij1lem15 9990	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐵 ∧ ¬ 𝑏 ∈ 𝐴)) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
127	121, 122, 123, 124, 125, 126	syl23anc 1376	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
128	120, 127	pm2.21dd 194	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
129	128	3exp 1118	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
130	118, 129	pm2.61d 179	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
131		simp13 1204	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
132		simp12l 1285	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
133		simp12r 1286	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
134		simp11 1202	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
135		simp2 1136	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
136		simp3 1137	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐵)
137	63	ackbij1lem15 9990	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
138	132, 133, 134, 135, 136, 137	syl23anc 1376	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
139	131, 138	pm2.21dd 194	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
140	139	3exp 1118	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
141		simp13 1204	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
142		ackbij1lem1 9976	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
143	142	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
144	143	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ 𝑏)))
145		ackbij1lem1 9976	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
146	145	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
147	146	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
148	144, 147	eqeq12d 2754	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
149	148	biimpd 228	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
150	149	3adant1 1129	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
151	141, 150	mpd 15	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
152	143, 146	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
153	152	biimprd 247	. . . . . . . . . . . 12 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
154	153	3adant1 1129	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
155	151, 154	embantd 59	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
156	155	3exp 1118	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
157	140, 156	pm2.61d 179	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
158	130, 157	pm2.61d 179	. . . . . . 7 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
159	158	3exp 1118	. . . . . 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 7745	. . 3 ⊢ (suc ∪ (𝐴 ∪ 𝐵) ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
163	17, 162	mpcom 38	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
164		omsson 7716	. . . . . . . 8 ⊢ ω ⊆ On
165	8, 164	sstrdi 3933	. . . . . . 7 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ On)
166		onsucuni 7675	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ⊆ On → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
167	165, 166	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
168	167	unssad 4121	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵))
169		df-ss 3904	. . . . 5 ⊢ (𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
170	168, 169	sylib 217	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
171	170	fveq2d 6778	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐴))
172	167	unssbd 4122	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵))
173		df-ss 3904	. . . . 5 ⊢ (𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
174	172, 173	sylib 217	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
175	174	fveq2d 6778	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐵))
176	171, 175	eqeq12d 2754	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) ↔ (𝐹‘𝐴) = (𝐹‘𝐵)))
177	170, 174	eqeq12d 2754	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) ↔ 𝐴 = 𝐵))
178	163, 176, 177	3imtr3d 293	1 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 𝒫 cpw 4533 {csn 4561 ∪ cuni 4839 ∪ ciun 4924 ↦ cmpt 5157 × cxp 5587 Ord word 6265 Oncon0 6266 suc csuc 6268 ‘cfv 6433 (class class class)co 7275 ωcom 7712 +_o coa 8294 Fincfn 8733 cardccrd 9693

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 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 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-oadd 8301 df-er 8498 df-map 8617 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-dju 9659 df-card 9697

This theorem is referenced by: ackbij1lem17 9992

W3C validator