ackbij1lem16

		Ref	Expression
	Hypothesis	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	Assertion	ackbij1lem16	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A) = F (B) \to A = B)$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2		inss1	$⊢ 𝒫 ω \cap Fin \subseteq 𝒫 ω$
3	2	sseli	$⊢ A \in (𝒫 ω \cap Fin) \to A \in 𝒫 ω$
4	3	elpwid	$⊢ A \in (𝒫 ω \cap Fin) \to A \subseteq ω$
5	4	adantr	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \subseteq ω$
6	2	sseli	$⊢ B \in (𝒫 ω \cap Fin) \to B \in 𝒫 ω$
7	6	elpwid	$⊢ B \in (𝒫 ω \cap Fin) \to B \subseteq ω$
8	7	adantl	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to B \subseteq ω$
9	5 8	unssd	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \subseteq ω$
10		inss2	$⊢ 𝒫 ω \cap Fin \subseteq Fin$
11	10	sseli	$⊢ A \in (𝒫 ω \cap Fin) \to A \in Fin$
12	10	sseli	$⊢ B \in (𝒫 ω \cap Fin) \to B \in Fin$
13		unfi	$⊢ (A \in Fin \land B \in Fin) \to A \cup B \in Fin$
14	11 12 13	syl2an	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \in Fin$
15		nnunifi	$⊢ (A \cup B \subseteq ω \land A \cup B \in Fin) \to ⋃ (A \cup B) \in ω$
16	9 14 15	syl2anc	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to ⋃ (A \cup B) \in ω$
17		peano2	$⊢ ⋃ (A \cup B) \in ω \to suc ⋃ (A \cup B) \in ω$
18	16 17	syl	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to suc ⋃ (A \cup B) \in ω$
19		ineq2	$⊢ a = \emptyset \to A \cap a = A \cap \emptyset$
20	19	fveq2d	$⊢ a = \emptyset \to F (A \cap a) = F (A \cap \emptyset)$
21		ineq2	$⊢ a = \emptyset \to B \cap a = B \cap \emptyset$
22	21	fveq2d	$⊢ a = \emptyset \to F (B \cap a) = F (B \cap \emptyset)$
23	20 22	eqeq12d	$⊢ a = \emptyset \to (F (A \cap a) = F (B \cap a) \leftrightarrow F (A \cap \emptyset) = F (B \cap \emptyset))$
24	19 21	eqeq12d	$⊢ a = \emptyset \to (A \cap a = B \cap a \leftrightarrow A \cap \emptyset = B \cap \emptyset)$
25	23 24	imbi12d	$⊢ a = \emptyset \to ((F (A \cap a) = F (B \cap a) \to A \cap a = B \cap a) \leftrightarrow (F (A \cap \emptyset) = F (B \cap \emptyset) \to A \cap \emptyset = B \cap \emptyset))$
26	25	imbi2d	$⊢ a = \emptyset \to (((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap a) = F (B \cap a) \to A \cap a = B \cap a)) \leftrightarrow ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap \emptyset) = F (B \cap \emptyset) \to A \cap \emptyset = B \cap \emptyset)))$
27		ineq2	$⊢ a = b \to A \cap a = A \cap b$
28	27	fveq2d	$⊢ a = b \to F (A \cap a) = F (A \cap b)$
29		ineq2	$⊢ a = b \to B \cap a = B \cap b$
30	29	fveq2d	$⊢ a = b \to F (B \cap a) = F (B \cap b)$
31	28 30	eqeq12d	$⊢ a = b \to (F (A \cap a) = F (B \cap a) \leftrightarrow F (A \cap b) = F (B \cap b))$
32	27 29	eqeq12d	$⊢ a = b \to (A \cap a = B \cap a \leftrightarrow A \cap b = B \cap b)$
33	31 32	imbi12d	$⊢ a = b \to ((F (A \cap a) = F (B \cap a) \to A \cap a = B \cap a) \leftrightarrow (F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b))$
34	33	imbi2d	$⊢ a = b \to (((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap a) = F (B \cap a) \to A \cap a = B \cap a)) \leftrightarrow ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b)))$
35		ineq2	$⊢ a = suc b \to A \cap a = A \cap suc b$
36	35	fveq2d	$⊢ a = suc b \to F (A \cap a) = F (A \cap suc b)$
37		ineq2	$⊢ a = suc b \to B \cap a = B \cap suc b$
38	37	fveq2d	$⊢ a = suc b \to F (B \cap a) = F (B \cap suc b)$
39	36 38	eqeq12d	$⊢ a = suc b \to (F (A \cap a) = F (B \cap a) \leftrightarrow F (A \cap suc b) = F (B \cap suc b))$
40	35 37	eqeq12d	$⊢ a = suc b \to (A \cap a = B \cap a \leftrightarrow A \cap suc b = B \cap suc b)$
41	39 40	imbi12d	$⊢ a = suc b \to ((F (A \cap a) = F (B \cap a) \to A \cap a = B \cap a) \leftrightarrow (F (A \cap suc b) = F (B \cap suc b) \to A \cap suc b = B \cap suc b))$
42	41	imbi2d	$⊢ a = suc b \to (((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap a) = F (B \cap a) \to A \cap a = B \cap a)) \leftrightarrow ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap suc b) = F (B \cap suc b) \to A \cap suc b = B \cap suc b)))$
43		ineq2	$⊢ a = suc ⋃ (A \cup B) \to A \cap a = A \cap suc ⋃ (A \cup B)$
44	43	fveq2d	$⊢ a = suc ⋃ (A \cup B) \to F (A \cap a) = F (A \cap suc ⋃ (A \cup B))$
45		ineq2	$⊢ a = suc ⋃ (A \cup B) \to B \cap a = B \cap suc ⋃ (A \cup B)$
46	45	fveq2d	$⊢ a = suc ⋃ (A \cup B) \to F (B \cap a) = F (B \cap suc ⋃ (A \cup B))$
47	44 46	eqeq12d	$⊢ a = suc ⋃ (A \cup B) \to (F (A \cap a) = F (B \cap a) \leftrightarrow F (A \cap suc ⋃ (A \cup B)) = F (B \cap suc ⋃ (A \cup B)))$
48	43 45	eqeq12d	$⊢ a = suc ⋃ (A \cup B) \to (A \cap a = B \cap a \leftrightarrow A \cap suc ⋃ (A \cup B) = B \cap suc ⋃ (A \cup B))$
49	47 48	imbi12d	$⊢ a = suc ⋃ (A \cup B) \to ((F (A \cap a) = F (B \cap a) \to A \cap a = B \cap a) \leftrightarrow (F (A \cap suc ⋃ (A \cup B)) = F (B \cap suc ⋃ (A \cup B)) \to A \cap suc ⋃ (A \cup B) = B \cap suc ⋃ (A \cup B)))$
50	49	imbi2d	$⊢ a = suc ⋃ (A \cup B) \to (((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap a) = F (B \cap a) \to A \cap a = B \cap a)) \leftrightarrow ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap suc ⋃ (A \cup B)) = F (B \cap suc ⋃ (A \cup B)) \to A \cap suc ⋃ (A \cup B) = B \cap suc ⋃ (A \cup B))))$
51		in0	$⊢ A \cap \emptyset = \emptyset$
52		in0	$⊢ B \cap \emptyset = \emptyset$
53	51 52	eqtr4i	$⊢ A \cap \emptyset = B \cap \emptyset$
54	53	2a1i	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap \emptyset) = F (B \cap \emptyset) \to A \cap \emptyset = B \cap \emptyset)$
55		simp13	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land b \in B) \to F (A \cap suc b) = F (B \cap suc b)$
56		3simpa	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \to (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)))$
57		ackbij1lem2	$⊢ b \in A \to A \cap suc b = \{b\} \cup (A \cap b)$
58	57	fveq2d	$⊢ b \in A \to F (A \cap suc b) = F (\{b\} \cup (A \cap b))$
59	58	3ad2ant2	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \land b \in A \land b \in B) \to F (A \cap suc b) = F (\{b\} \cup (A \cap b))$
60		ackbij1lem4	$⊢ b \in ω \to \{b\} \in (𝒫 ω \cap Fin)$
61	60	adantr	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to \{b\} \in (𝒫 ω \cap Fin)$
62		simprl	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to A \in (𝒫 ω \cap Fin)$
63		inss1	$⊢ A \cap b \subseteq A$
64	1	ackbij1lem11	$⊢ (A \in (𝒫 ω \cap Fin) \land A \cap b \subseteq A) \to A \cap b \in (𝒫 ω \cap Fin)$
65	62 63 64	sylancl	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to A \cap b \in (𝒫 ω \cap Fin)$
66		incom	$⊢ \{b\} \cap (A \cap b) = (A \cap b) \cap \{b\}$
67		inss2	$⊢ A \cap b \subseteq b$
68		nnord	$⊢ b \in ω \to Ord b$
69		orddisj	$⊢ Ord b \to b \cap \{b\} = \emptyset$
70	68 69	syl	$⊢ b \in ω \to b \cap \{b\} = \emptyset$
71	70	adantr	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to b \cap \{b\} = \emptyset$
72		ssdisj	$⊢ (A \cap b \subseteq b \land b \cap \{b\} = \emptyset) \to (A \cap b) \cap \{b\} = \emptyset$
73	67 71 72	sylancr	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to (A \cap b) \cap \{b\} = \emptyset$
74	66 73	eqtrid	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to \{b\} \cap (A \cap b) = \emptyset$
75	1	ackbij1lem9	$⊢ (\{b\} \in (𝒫 ω \cap Fin) \land A \cap b \in (𝒫 ω \cap Fin) \land \{b\} \cap (A \cap b) = \emptyset) \to F (\{b\} \cup (A \cap b)) = F (\{b\}) +_{𝑜} F (A \cap b)$
76	61 65 74 75	syl3anc	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to F (\{b\} \cup (A \cap b)) = F (\{b\}) +_{𝑜} F (A \cap b)$
77	76	3ad2ant1	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \land b \in A \land b \in B) \to F (\{b\} \cup (A \cap b)) = F (\{b\}) +_{𝑜} F (A \cap b)$
78	59 77	eqtrd	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \land b \in A \land b \in B) \to F (A \cap suc b) = F (\{b\}) +_{𝑜} F (A \cap b)$
79	56 78	syl3an1	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land b \in B) \to F (A \cap suc b) = F (\{b\}) +_{𝑜} F (A \cap b)$
80		ackbij1lem2	$⊢ b \in B \to B \cap suc b = \{b\} \cup (B \cap b)$
81	80	fveq2d	$⊢ b \in B \to F (B \cap suc b) = F (\{b\} \cup (B \cap b))$
82	81	3ad2ant3	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \land b \in A \land b \in B) \to F (B \cap suc b) = F (\{b\} \cup (B \cap b))$
83		simprr	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to B \in (𝒫 ω \cap Fin)$
84		inss1	$⊢ B \cap b \subseteq B$
85	1	ackbij1lem11	$⊢ (B \in (𝒫 ω \cap Fin) \land B \cap b \subseteq B) \to B \cap b \in (𝒫 ω \cap Fin)$
86	83 84 85	sylancl	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to B \cap b \in (𝒫 ω \cap Fin)$
87		incom	$⊢ \{b\} \cap (B \cap b) = (B \cap b) \cap \{b\}$
88		inss2	$⊢ B \cap b \subseteq b$
89		ssdisj	$⊢ (B \cap b \subseteq b \land b \cap \{b\} = \emptyset) \to (B \cap b) \cap \{b\} = \emptyset$
90	88 71 89	sylancr	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to (B \cap b) \cap \{b\} = \emptyset$
91	87 90	eqtrid	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to \{b\} \cap (B \cap b) = \emptyset$
92	1	ackbij1lem9	$⊢ (\{b\} \in (𝒫 ω \cap Fin) \land B \cap b \in (𝒫 ω \cap Fin) \land \{b\} \cap (B \cap b) = \emptyset) \to F (\{b\} \cup (B \cap b)) = F (\{b\}) +_{𝑜} F (B \cap b)$
93	61 86 91 92	syl3anc	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to F (\{b\} \cup (B \cap b)) = F (\{b\}) +_{𝑜} F (B \cap b)$
94	93	3ad2ant1	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \land b \in A \land b \in B) \to F (\{b\} \cup (B \cap b)) = F (\{b\}) +_{𝑜} F (B \cap b)$
95	82 94	eqtrd	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \land b \in A \land b \in B) \to F (B \cap suc b) = F (\{b\}) +_{𝑜} F (B \cap b)$
96	56 95	syl3an1	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land b \in B) \to F (B \cap suc b) = F (\{b\}) +_{𝑜} F (B \cap b)$
97	55 79 96	3eqtr3d	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land b \in B) \to F (\{b\}) +_{𝑜} F (A \cap b) = F (\{b\}) +_{𝑜} F (B \cap b)$
98	1	ackbij1lem10	$⊢ F : 𝒫 ω \cap Fin ⟶ ω$
99	98	ffvelcdmi	$⊢ \{b\} \in (𝒫 ω \cap Fin) \to F (\{b\}) \in ω$
100	61 99	syl	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to F (\{b\}) \in ω$
101	98	ffvelcdmi	$⊢ A \cap b \in (𝒫 ω \cap Fin) \to F (A \cap b) \in ω$
102	65 101	syl	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to F (A \cap b) \in ω$
103	98	ffvelcdmi	$⊢ B \cap b \in (𝒫 ω \cap Fin) \to F (B \cap b) \in ω$
104	86 103	syl	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to F (B \cap b) \in ω$
105		nnacan	$⊢ (F (\{b\}) \in ω \land F (A \cap b) \in ω \land F (B \cap b) \in ω) \to (F (\{b\}) +_{𝑜} F (A \cap b) = F (\{b\}) +_{𝑜} F (B \cap b) \leftrightarrow F (A \cap b) = F (B \cap b))$
106	100 102 104 105	syl3anc	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin))) \to (F (\{b\}) +_{𝑜} F (A \cap b) = F (\{b\}) +_{𝑜} F (B \cap b) \leftrightarrow F (A \cap b) = F (B \cap b))$
107	106	3adant3	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \to (F (\{b\}) +_{𝑜} F (A \cap b) = F (\{b\}) +_{𝑜} F (B \cap b) \leftrightarrow F (A \cap b) = F (B \cap b))$
108	107	3ad2ant1	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land b \in B) \to (F (\{b\}) +_{𝑜} F (A \cap b) = F (\{b\}) +_{𝑜} F (B \cap b) \leftrightarrow F (A \cap b) = F (B \cap b))$
109	97 108	mpbid	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land b \in B) \to F (A \cap b) = F (B \cap b)$
110		uneq2	$⊢ A \cap b = B \cap b \to \{b\} \cup (A \cap b) = \{b\} \cup (B \cap b)$
111	110	adantl	$⊢ ((b \in A \land b \in B) \land A \cap b = B \cap b) \to \{b\} \cup (A \cap b) = \{b\} \cup (B \cap b)$
112	57	ad2antrr	$⊢ ((b \in A \land b \in B) \land A \cap b = B \cap b) \to A \cap suc b = \{b\} \cup (A \cap b)$
113	80	ad2antlr	$⊢ ((b \in A \land b \in B) \land A \cap b = B \cap b) \to B \cap suc b = \{b\} \cup (B \cap b)$
114	111 112 113	3eqtr4d	$⊢ ((b \in A \land b \in B) \land A \cap b = B \cap b) \to A \cap suc b = B \cap suc b$
115	114	ex	$⊢ (b \in A \land b \in B) \to (A \cap b = B \cap b \to A \cap suc b = B \cap suc b)$
116	115	3adant1	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land b \in B) \to (A \cap b = B \cap b \to A \cap suc b = B \cap suc b)$
117	109 116	embantd	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land b \in B) \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)$
118	117	3exp	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \to (b \in A \to (b \in B \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)))$
119		simp13	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land b \in B) \to F (A \cap suc b) = F (B \cap suc b)$
120	119	eqcomd	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land b \in B) \to F (B \cap suc b) = F (A \cap suc b)$
121		simp12r	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land b \in B) \to B \in (𝒫 ω \cap Fin)$
122		simp12l	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land b \in B) \to A \in (𝒫 ω \cap Fin)$
123		simp11	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land b \in B) \to b \in ω$
124		simp3	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land b \in B) \to b \in B$
125		simp2	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land b \in B) \to \neg b \in A$
126	1	ackbij1lem15	$⊢ ((B \in (𝒫 ω \cap Fin) \land A \in (𝒫 ω \cap Fin)) \land (b \in ω \land b \in B \land \neg b \in A)) \to \neg F (B \cap suc b) = F (A \cap suc b)$
127	121 122 123 124 125 126	syl23anc	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land b \in B) \to \neg F (B \cap suc b) = F (A \cap suc b)$
128	120 127	pm2.21dd	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land b \in B) \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)$
129	128	3exp	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \to (\neg b \in A \to (b \in B \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)))$
130	118 129	pm2.61d	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \to (b \in B \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b))$
131		simp13	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land \neg b \in B) \to F (A \cap suc b) = F (B \cap suc b)$
132		simp12l	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land \neg b \in B) \to A \in (𝒫 ω \cap Fin)$
133		simp12r	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land \neg b \in B) \to B \in (𝒫 ω \cap Fin)$
134		simp11	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land \neg b \in B) \to b \in ω$
135		simp2	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land \neg b \in B) \to b \in A$
136		simp3	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land \neg b \in B) \to \neg b \in B$
137	1	ackbij1lem15	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (b \in ω \land b \in A \land \neg b \in B)) \to \neg F (A \cap suc b) = F (B \cap suc b)$
138	132 133 134 135 136 137	syl23anc	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land \neg b \in B) \to \neg F (A \cap suc b) = F (B \cap suc b)$
139	131 138	pm2.21dd	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land b \in A \land \neg b \in B) \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)$
140	139	3exp	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \to (b \in A \to (\neg b \in B \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)))$
141		simp13	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land \neg b \in B) \to F (A \cap suc b) = F (B \cap suc b)$
142		ackbij1lem1	$⊢ \neg b \in A \to A \cap suc b = A \cap b$
143	142	adantr	$⊢ (\neg b \in A \land \neg b \in B) \to A \cap suc b = A \cap b$
144	143	fveq2d	$⊢ (\neg b \in A \land \neg b \in B) \to F (A \cap suc b) = F (A \cap b)$
145		ackbij1lem1	$⊢ \neg b \in B \to B \cap suc b = B \cap b$
146	145	adantl	$⊢ (\neg b \in A \land \neg b \in B) \to B \cap suc b = B \cap b$
147	146	fveq2d	$⊢ (\neg b \in A \land \neg b \in B) \to F (B \cap suc b) = F (B \cap b)$
148	144 147	eqeq12d	$⊢ (\neg b \in A \land \neg b \in B) \to (F (A \cap suc b) = F (B \cap suc b) \leftrightarrow F (A \cap b) = F (B \cap b))$
149	148	biimpd	$⊢ (\neg b \in A \land \neg b \in B) \to (F (A \cap suc b) = F (B \cap suc b) \to F (A \cap b) = F (B \cap b))$
150	149	3adant1	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land \neg b \in B) \to (F (A \cap suc b) = F (B \cap suc b) \to F (A \cap b) = F (B \cap b))$
151	141 150	mpd	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land \neg b \in B) \to F (A \cap b) = F (B \cap b)$
152	143 146	eqeq12d	$⊢ (\neg b \in A \land \neg b \in B) \to (A \cap suc b = B \cap suc b \leftrightarrow A \cap b = B \cap b)$
153	152	biimprd	$⊢ (\neg b \in A \land \neg b \in B) \to (A \cap b = B \cap b \to A \cap suc b = B \cap suc b)$
154	153	3adant1	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land \neg b \in B) \to (A \cap b = B \cap b \to A \cap suc b = B \cap suc b)$
155	151 154	embantd	$⊢ ((b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \land \neg b \in A \land \neg b \in B) \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)$
156	155	3exp	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \to (\neg b \in A \to (\neg b \in B \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)))$
157	140 156	pm2.61d	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \to (\neg b \in B \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b))$
158	130 157	pm2.61d	$⊢ (b \in ω \land (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land F (A \cap suc b) = F (B \cap suc b)) \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)$
159	158	3exp	$⊢ b \in ω \to ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap suc b) = F (B \cap suc b) \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to A \cap suc b = B \cap suc b)))$
160	159	com34	$⊢ b \in ω \to ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to ((F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b) \to (F (A \cap suc b) = F (B \cap suc b) \to A \cap suc b = B \cap suc b)))$
161	160	a2d	$⊢ b \in ω \to (((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap b) = F (B \cap b) \to A \cap b = B \cap b)) \to ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap suc b) = F (B \cap suc b) \to A \cap suc b = B \cap suc b)))$
162	26 34 42 50 54 161	finds	$⊢ suc ⋃ (A \cup B) \in ω \to ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap suc ⋃ (A \cup B)) = F (B \cap suc ⋃ (A \cup B)) \to A \cap suc ⋃ (A \cup B) = B \cap suc ⋃ (A \cup B)))$
163	18 162	mpcom	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap suc ⋃ (A \cup B)) = F (B \cap suc ⋃ (A \cup B)) \to A \cap suc ⋃ (A \cup B) = B \cap suc ⋃ (A \cup B))$
164		omsson	$⊢ ω \subseteq On$
165	9 164	sstrdi	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \subseteq On$
166		onsucuni	$⊢ A \cup B \subseteq On \to A \cup B \subseteq suc ⋃ (A \cup B)$
167	165 166	syl	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \subseteq suc ⋃ (A \cup B)$
168	167	unssad	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \subseteq suc ⋃ (A \cup B)$
169		df-ss	$⊢ A \subseteq suc ⋃ (A \cup B) \leftrightarrow A \cap suc ⋃ (A \cup B) = A$
170	168 169	sylib	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cap suc ⋃ (A \cup B) = A$
171	170	fveq2d	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to F (A \cap suc ⋃ (A \cup B)) = F (A)$
172	167	unssbd	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to B \subseteq suc ⋃ (A \cup B)$
173		df-ss	$⊢ B \subseteq suc ⋃ (A \cup B) \leftrightarrow B \cap suc ⋃ (A \cup B) = B$
174	172 173	sylib	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to B \cap suc ⋃ (A \cup B) = B$
175	174	fveq2d	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to F (B \cap suc ⋃ (A \cup B)) = F (B)$
176	171 175	eqeq12d	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A \cap suc ⋃ (A \cup B)) = F (B \cap suc ⋃ (A \cup B)) \leftrightarrow F (A) = F (B))$
177	170 174	eqeq12d	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (A \cap suc ⋃ (A \cup B) = B \cap suc ⋃ (A \cup B) \leftrightarrow A = B)$
178	163 176 177	3imtr3d	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to (F (A) = F (B) \to A = B)$

Metamath Proof Explorer

Theorem ackbij1lem16

Proof