f1otrg - Metamath Proof Explorer

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

Theorem f1otrg 27232

Description: A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019.)

**Hypotheses**
Ref	Expression
f1otrkg.p	⊢ 𝑃 = (Base‘𝐺)
f1otrkg.d	⊢ 𝐷 = (dist‘𝐺)
f1otrkg.i	⊢ 𝐼 = (Itv‘𝐺)
f1otrkg.b	⊢ 𝐵 = (Base‘𝐻)
f1otrkg.e	⊢ 𝐸 = (dist‘𝐻)
f1otrkg.j	⊢ 𝐽 = (Itv‘𝐻)
f1otrkg.f	⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)
f1otrkg.1	⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
f1otrkg.2	⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
f1otrg.h	⊢ (𝜑 → 𝐻 ∈ 𝑉)
f1otrg.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
f1otrg.l	⊢ (𝜑 → (LineG‘𝐻) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))

**Assertion**
Ref	Expression
f1otrg	⊢ (𝜑 → 𝐻 ∈ TarskiG)

Distinct variable groups: 𝑒,𝑓,𝑔,𝑥,𝑦,𝑧,𝐵 𝐷,𝑒,𝑓,𝑔 𝑒,𝐸,𝑓,𝑔,𝑥,𝑦,𝑧 𝑒,𝐹,𝑓,𝑔,𝑥,𝑦,𝑧 𝑒,𝐼,𝑓,𝑔,𝑥,𝑦 𝑒,𝐽,𝑓,𝑔,𝑥,𝑦,𝑧 𝑃,𝑒,𝑓,𝑔,𝑥,𝑦,𝑧 𝜑,𝑒,𝑓,𝑔,𝑥,𝑦,𝑧 𝑓,𝐻 Allowed substitution hints: 𝐷(𝑥,𝑦,𝑧) 𝐺(𝑥,𝑦,𝑧,𝑒,𝑓,𝑔) 𝐻(𝑥,𝑦,𝑧,𝑒,𝑔) 𝐼(𝑧) 𝑉(𝑥,𝑦,𝑧,𝑒,𝑓,𝑔)

Proof of Theorem f1otrg Dummy variables 𝑎 𝑏 𝑐 𝑖 𝑝 𝑠 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1otrg.h	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ 𝑉)
2	1	elexd 3452	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ V)
3		f1otrkg.p	. . . . . . . . 9 ⊢ 𝑃 = (Base‘𝐺)
4		f1otrkg.d	. . . . . . . . 9 ⊢ 𝐷 = (dist‘𝐺)
5		f1otrkg.i	. . . . . . . . 9 ⊢ 𝐼 = (Itv‘𝐺)
6		f1otrg.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	6	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ TarskiG)
8		f1otrkg.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)
9		f1of 6716	. . . . . . . . . . . 12 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃)
10	8, 9	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐵⟶𝑃)
11	10	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃)
12		simprl 768	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵)
13	11, 12	ffvelrnd 6962	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃)
14		simprr 770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
15	11, 14	ffvelrnd 6962	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃)
16	3, 4, 5, 7, 13, 15	axtgcgrrflx 26823	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘𝑦)𝐷(𝐹‘𝑥)))
17		f1otrkg.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐻)
18		f1otrkg.e	. . . . . . . . 9 ⊢ 𝐸 = (dist‘𝐻)
19		f1otrkg.j	. . . . . . . . 9 ⊢ 𝐽 = (Itv‘𝐻)
20	8	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵–1-1-onto→𝑃)
21		f1otrkg.1	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
22	21	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
23		f1otrkg.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
24	23	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
25	3, 4, 5, 17, 18, 19, 20, 22, 24, 12, 14	f1otrgds 27230	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐸𝑦) = ((𝐹‘𝑥)𝐷(𝐹‘𝑦)))
26	3, 4, 5, 17, 18, 19, 20, 22, 24, 14, 12	f1otrgds 27230	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦𝐸𝑥) = ((𝐹‘𝑦)𝐷(𝐹‘𝑥)))
27	16, 25, 26	3eqtr4d 2788	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
28	27	ralrimivva 3123	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
29		f1of1 6715	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵–1-1→𝑃)
30	8, 29	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵–1-1→𝑃)
31	30	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵–1-1→𝑃)
32		simp21 1205	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 ∈ 𝐵)
33		simp22 1206	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑦 ∈ 𝐵)
34	32, 33	jca 512	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
35	6	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐺 ∈ TarskiG)
36	10	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵⟶𝑃)
37	36, 32	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑥) ∈ 𝑃)
38	36, 33	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑦) ∈ 𝑃)
39		simp23 1207	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑧 ∈ 𝐵)
40	36, 39	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑧) ∈ 𝑃)
41		simp3 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = (𝑧𝐸𝑧))
42	8	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵–1-1-onto→𝑃)
43	21	3ad2antl1 1184	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
44	23	3ad2antl1 1184	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
45	3, 4, 5, 17, 18, 19, 42, 43, 44, 32, 33	f1otrgds 27230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = ((𝐹‘𝑥)𝐷(𝐹‘𝑦)))
46	3, 4, 5, 17, 18, 19, 42, 43, 44, 39, 39	f1otrgds 27230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑧𝐸𝑧) = ((𝐹‘𝑧)𝐷(𝐹‘𝑧)))
47	41, 45, 46	3eqtr3d 2786	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘𝑧)𝐷(𝐹‘𝑧)))
48	3, 4, 5, 35, 37, 38, 40, 47	axtgcgrid 26824	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑥) = (𝐹‘𝑦))
49		f1veqaeq 7130	. . . . . . . . . 10 ⊢ ((𝐹:𝐵–1-1→𝑃 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
50	49	imp 407	. . . . . . . . 9 ⊢ (((𝐹:𝐵–1-1→𝑃 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 = 𝑦)
51	31, 34, 48, 50	syl21anc 835	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 = 𝑦)
52	51	3expia 1120	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
53	52	ralrimivvva 3127	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
54	28, 53	jca 512	. . . . 5 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)))
55	17, 18, 19	istrkgc 26815	. . . . 5 ⊢ (𝐻 ∈ TarskiG_C ↔ (𝐻 ∈ V ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))))
56	2, 54, 55	sylanbrc 583	. . . 4 ⊢ (𝜑 → 𝐻 ∈ TarskiG_C)
57	8	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵–1-1-onto→𝑃)
58	57, 29	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵–1-1→𝑃)
59		simp2 1136	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
60	6	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐺 ∈ TarskiG)
61	13	3adant3 1131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑥) ∈ 𝑃)
62	15	3adant3 1131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑦) ∈ 𝑃)
63		simp3 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ (𝑥𝐽𝑥))
64	21	3ad2antl1 1184	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
65	23	3ad2antl1 1184	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
66	12	3adant3 1131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 ∈ 𝐵)
67	14	3adant3 1131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ 𝐵)
68	3, 4, 5, 17, 18, 19, 57, 64, 65, 66, 66, 67	f1otrgitv 27231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑦 ∈ (𝑥𝐽𝑥) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑥))))
69	63, 68	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑥)))
70	3, 4, 5, 60, 61, 62, 69	axtgbtwnid 26827	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑥) = (𝐹‘𝑦))
71	58, 59, 70, 50	syl21anc 835	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 = 𝑦)
72	71	3expia 1120	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
73	72	ralrimivva 3123	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
74		f1ocnv 6728	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ^◡𝐹:𝑃–1-1-onto→𝐵)
75		f1of 6716	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹:𝑃–1-1-onto→𝐵 → ^◡𝐹:𝑃⟶𝐵)
76	8, 74, 75	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ^◡𝐹:𝑃⟶𝐵)
77	76	ad5antr 731	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ^◡𝐹:𝑃⟶𝐵)
78		simplr 766	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑐 ∈ 𝑃)
79	77, 78	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (^◡𝐹‘𝑐) ∈ 𝐵)
80		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (^◡𝐹‘𝑐)) → 𝑎 = (^◡𝐹‘𝑐))
81	80	eleq1d 2823	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (^◡𝐹‘𝑐)) → (𝑎 ∈ (𝑢𝐽𝑦) ↔ (^◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦)))
82	80	eleq1d 2823	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (^◡𝐹‘𝑐)) → (𝑎 ∈ (𝑣𝐽𝑥) ↔ (^◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥)))
83	81, 82	anbi12d 631	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (^◡𝐹‘𝑐)) → ((𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)) ↔ ((^◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦) ∧ (^◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥))))
84		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)))
85	20	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵–1-1-onto→𝑃)
86	85	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝐹:𝐵–1-1-onto→𝑃)
87		f1ocnvfv2 7149	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
88	87	eleq1d 2823	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → ((𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ↔ 𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦))))
89	86, 78, 88	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ↔ 𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦))))
90	84, 89	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)))
91	22	ad4ant14 749	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
92	91	ad4ant14 749	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
93	24	ad4ant14 749	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
94	93	ad4ant14 749	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
95		simplr2 1215	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ 𝐵)
96	95	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑢 ∈ 𝐵)
97	14	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑦 ∈ 𝐵)
98	97	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑦 ∈ 𝐵)
99	3, 4, 5, 17, 18, 19, 86, 92, 94, 96, 98, 79	f1otrgitv 27231	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((^◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦) ↔ (𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦))))
100	90, 99	mpbird 256	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (^◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦))
101		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))
102	87	eleq1d 2823	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → ((𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)) ↔ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥))))
103	86, 78, 102	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)) ↔ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥))))
104	101, 103	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))
105		simplr3 1216	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ 𝐵)
106	105	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑣 ∈ 𝐵)
107	12	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑥 ∈ 𝐵)
108	107	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑥 ∈ 𝐵)
109	3, 4, 5, 17, 18, 19, 86, 92, 94, 106, 108, 79	f1otrgitv 27231	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((^◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥) ↔ (𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥))))
110	104, 109	mpbird 256	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (^◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥))
111	100, 110	jca 512	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((^◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦) ∧ (^◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥)))
112	79, 83, 111	rspcedvd 3563	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
113	7	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐺 ∈ TarskiG)
114	11	ad2antrr 723	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵⟶𝑃)
115	114, 107	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑥) ∈ 𝑃)
116	114, 97	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑦) ∈ 𝑃)
117		simplr1 1214	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑧 ∈ 𝐵)
118	114, 117	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑧) ∈ 𝑃)
119	114, 95	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑢) ∈ 𝑃)
120	114, 105	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑣) ∈ 𝑃)
121		simprl 768	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ (𝑥𝐽𝑧))
122	3, 4, 5, 17, 18, 19, 85, 91, 93, 107, 117, 95	f1otrgitv 27231	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑢 ∈ (𝑥𝐽𝑧) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧))))
123	121, 122	mpbid 231	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧)))
124		simprr 770	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ (𝑦𝐽𝑧))
125	3, 4, 5, 17, 18, 19, 85, 91, 93, 97, 117, 105	f1otrgitv 27231	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑣 ∈ (𝑦𝐽𝑧) ↔ (𝐹‘𝑣) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧))))
126	124, 125	mpbid 231	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑣) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧)))
127	3, 4, 5, 113, 115, 116, 118, 119, 120, 123, 126	axtgpasch 26828	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑐 ∈ 𝑃 (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥))))
128	112, 127	r19.29a 3218	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
129	128	ex 413	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
130	129	ralrimivvva 3127	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
131	130	ralrimivva 3123	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
132	8	ad5antr 731	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝐹:𝐵–1-1-onto→𝑃)
133		simpllr 773	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑐 ∈ 𝑃)
134	132, 133, 87	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
135		ffn 6600	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐵⟶𝑃 → 𝐹 Fn 𝐵)
136	132, 9, 135	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝐹 Fn 𝐵)
137		simp-4r 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵))
138	137	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
139	138	elpwid 4544	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ⊆ 𝐵)
140	139	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ⊆ 𝐵)
141		simprl 768	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝑠)
142		fnfvima 7109	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn 𝐵 ∧ 𝑠 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑠) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑠))
143	136, 140, 141, 142	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑠))
144	137	simprd 496	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
145	144	elpwid 4544	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ⊆ 𝐵)
146	145	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ⊆ 𝐵)
147		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡)
148		fnfvima 7109	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn 𝐵 ∧ 𝑡 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑡) → (𝐹‘𝑦) ∈ (𝐹 “ 𝑡))
149	136, 146, 147, 148	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘𝑦) ∈ (𝐹 “ 𝑡))
150		simplr 766	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓))
151		oveq1 7282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝐹‘𝑥) → (𝑒𝐼𝑓) = ((𝐹‘𝑥)𝐼𝑓))
152	151	eleq2d 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝐹‘𝑥) → (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((𝐹‘𝑥)𝐼𝑓)))
153		oveq2 7283	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝐹‘𝑦) → ((𝐹‘𝑥)𝐼𝑓) = ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))
154	153	eleq2d 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝐹‘𝑦) → (𝑐 ∈ ((𝐹‘𝑥)𝐼𝑓) ↔ 𝑐 ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦))))
155	152, 154	rspc2va 3571	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) ∈ (𝐹 “ 𝑠) ∧ (𝐹‘𝑦) ∈ (𝐹 “ 𝑡)) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → 𝑐 ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))
156	143, 149, 150, 155	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑐 ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))
157	134, 156	eqeltrd 2839	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))
158	8	ad4antr 729	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝐹:𝐵–1-1-onto→𝑃)
159		simp-5l 782	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → 𝜑)
160	159, 21	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
161		simp-5l 782	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝜑)
162	161, 23	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
163		simprl 768	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝑠)
164	139, 163	sseldd 3922	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝐵)
165		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡)
166	145, 165	sseldd 3922	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝐵)
167	76	ad4antr 729	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ^◡𝐹:𝑃⟶𝐵)
168		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑐 ∈ 𝑃)
169	167, 168	ffvelrnd 6962	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (^◡𝐹‘𝑐) ∈ 𝐵)
170	3, 4, 5, 17, 18, 19, 158, 160, 162, 164, 166, 169	f1otrgitv 27231	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ((^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦))))
171	170	adantlr 712	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ((^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(^◡𝐹‘𝑐)) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦))))
172	157, 171	mpbird 256	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦))
173	172	ralrimivva 3123	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦))
174	173	adantllr 716	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦))
175	76	ad4antr 729	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → ^◡𝐹:𝑃⟶𝐵)
176		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → 𝑐 ∈ 𝑃)
177	175, 176	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → (^◡𝐹‘𝑐) ∈ 𝐵)
178		eleq1 2826	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (^◡𝐹‘𝑐) → (𝑏 ∈ (𝑥𝐽𝑦) ↔ (^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦)))
179	178	2ralbidv 3129	. . . . . . . . . . . . 13 ⊢ (𝑏 = (^◡𝐹‘𝑐) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦)))
180	179	adantl 482	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 = (^◡𝐹‘𝑐)) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦)))
181	177, 180	rspcedv 3554	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
182	181	adantr 481	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (^◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
183	174, 182	mpd 15	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))
184	6	ad3antrrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐺 ∈ TarskiG)
185		imassrn 5980	. . . . . . . . . . 11 ⊢ (𝐹 “ 𝑠) ⊆ ran 𝐹
186		f1ofo 6723	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵–onto→𝑃)
187		forn 6691	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵–onto→𝑃 → ran 𝐹 = 𝑃)
188	8, 186, 187	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐹 = 𝑃)
189	188	ad3antrrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ran 𝐹 = 𝑃)
190	185, 189	sseqtrid 3973	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹 “ 𝑠) ⊆ 𝑃)
191		imassrn 5980	. . . . . . . . . . 11 ⊢ (𝐹 “ 𝑡) ⊆ ran 𝐹
192	191, 189	sseqtrid 3973	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹 “ 𝑡) ⊆ 𝑃)
193	10	ad3antrrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐹:𝐵⟶𝑃)
194		simplr 766	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝑎 ∈ 𝐵)
195	193, 194	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹‘𝑎) ∈ 𝑃)
196	8	ad5antr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝐹:𝐵–1-1-onto→𝑃)
197		ffn 6600	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝐹:𝑃⟶𝐵 → ^◡𝐹 Fn 𝑃)
198	196, 74, 75, 197	4syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ^◡𝐹 Fn 𝑃)
199	190	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹 “ 𝑠) ⊆ 𝑃)
200		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ (𝐹 “ 𝑠))
201		fnfvima 7109	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐹 Fn 𝑃 ∧ (𝐹 “ 𝑠) ⊆ 𝑃 ∧ 𝑢 ∈ (𝐹 “ 𝑠)) → (^◡𝐹‘𝑢) ∈ (^◡𝐹 “ (𝐹 “ 𝑠)))
202	198, 199, 200, 201	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹‘𝑢) ∈ (^◡𝐹 “ (𝐹 “ 𝑠)))
203	196, 29	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝐹:𝐵–1-1→𝑃)
204		simp-5r 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵))
205	204	simpld 495	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
206	205	elpwid 4544	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑠 ⊆ 𝐵)
207		f1imacnv 6732	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐵–1-1→𝑃 ∧ 𝑠 ⊆ 𝐵) → (^◡𝐹 “ (𝐹 “ 𝑠)) = 𝑠)
208	203, 206, 207	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹 “ (𝐹 “ 𝑠)) = 𝑠)
209	202, 208	eleqtrd 2841	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹‘𝑢) ∈ 𝑠)
210	192	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹 “ 𝑡) ⊆ 𝑃)
211		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑣 ∈ (𝐹 “ 𝑡))
212		fnfvima 7109	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐹 Fn 𝑃 ∧ (𝐹 “ 𝑡) ⊆ 𝑃 ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹‘𝑣) ∈ (^◡𝐹 “ (𝐹 “ 𝑡)))
213	198, 210, 211, 212	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹‘𝑣) ∈ (^◡𝐹 “ (𝐹 “ 𝑡)))
214	204	simprd 496	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
215	214	elpwid 4544	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑡 ⊆ 𝐵)
216		f1imacnv 6732	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐵–1-1→𝑃 ∧ 𝑡 ⊆ 𝐵) → (^◡𝐹 “ (𝐹 “ 𝑡)) = 𝑡)
217	203, 215, 216	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹 “ (𝐹 “ 𝑡)) = 𝑡)
218	213, 217	eleqtrd 2841	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹‘𝑣) ∈ 𝑡)
219		simpllr 773	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦))
220		eleq1 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (^◡𝐹‘𝑢) → (𝑥 ∈ (𝑎𝐽𝑦) ↔ (^◡𝐹‘𝑢) ∈ (𝑎𝐽𝑦)))
221		oveq2 7283	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (^◡𝐹‘𝑣) → (𝑎𝐽𝑦) = (𝑎𝐽(^◡𝐹‘𝑣)))
222	221	eleq2d 2824	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (^◡𝐹‘𝑣) → ((^◡𝐹‘𝑢) ∈ (𝑎𝐽𝑦) ↔ (^◡𝐹‘𝑢) ∈ (𝑎𝐽(^◡𝐹‘𝑣))))
223	220, 222	rspc2va 3571	. . . . . . . . . . . . . 14 ⊢ ((((^◡𝐹‘𝑢) ∈ 𝑠 ∧ (^◡𝐹‘𝑣) ∈ 𝑡) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (^◡𝐹‘𝑢) ∈ (𝑎𝐽(^◡𝐹‘𝑣)))
224	209, 218, 219, 223	syl21anc 835	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹‘𝑢) ∈ (𝑎𝐽(^◡𝐹‘𝑣)))
225		simp-6l 784	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → 𝜑)
226	225, 21	sylancom 588	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
227		simp-6l 784	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝜑)
228	227, 23	sylancom 588	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
229		simp-4r 781	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑎 ∈ 𝐵)
230	210, 211	sseldd 3922	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑣 ∈ 𝑃)
231		f1ocnvdm 7157	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) → (^◡𝐹‘𝑣) ∈ 𝐵)
232	196, 230, 231	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹‘𝑣) ∈ 𝐵)
233	199, 200	sseldd 3922	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ 𝑃)
234		f1ocnvdm 7157	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑢 ∈ 𝑃) → (^◡𝐹‘𝑢) ∈ 𝐵)
235	196, 233, 234	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (^◡𝐹‘𝑢) ∈ 𝐵)
236	3, 4, 5, 17, 18, 19, 196, 226, 228, 229, 232, 235	f1otrgitv 27231	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ((^◡𝐹‘𝑢) ∈ (𝑎𝐽(^◡𝐹‘𝑣)) ↔ (𝐹‘(^◡𝐹‘𝑢)) ∈ ((𝐹‘𝑎)𝐼(𝐹‘(^◡𝐹‘𝑣)))))
237	224, 236	mpbid 231	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹‘(^◡𝐹‘𝑢)) ∈ ((𝐹‘𝑎)𝐼(𝐹‘(^◡𝐹‘𝑣))))
238		f1ocnvfv2 7149	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑢 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
239	196, 233, 238	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
240		f1ocnvfv2 7149	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
241	196, 230, 240	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
242	241	oveq2d 7291	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ((𝐹‘𝑎)𝐼(𝐹‘(^◡𝐹‘𝑣))) = ((𝐹‘𝑎)𝐼𝑣))
243	237, 239, 242	3eltr3d 2853	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ ((𝐹‘𝑎)𝐼𝑣))
244	243	3impa 1109	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ ((𝐹‘𝑎)𝐼𝑣))
245	3, 4, 5, 184, 190, 192, 195, 244	axtgcont 26830	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑐 ∈ 𝑃 ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓))
246	183, 245	r19.29a 3218	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))
247	246	rexlimdva2 3216	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
248	247	ralrimivva 3123	. . . . . 6 ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
249	73, 131, 248	3jca 1127	. . . . 5 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))))
250	17, 18, 19	istrkgb 26816	. . . . 5 ⊢ (𝐻 ∈ TarskiG_B ↔ (𝐻 ∈ V ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)))))
251	2, 249, 250	sylanbrc 583	. . . 4 ⊢ (𝜑 → 𝐻 ∈ TarskiG_B)
252	56, 251	elind 4128	. . 3 ⊢ (𝜑 → 𝐻 ∈ (TarskiG_C ∩ TarskiG_B))
253	6	ad9antr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐺 ∈ TarskiG)
254	10	ad9antr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵⟶𝑃)
255		simp-9r 791	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥 ∈ 𝐵)
256	254, 255	ffvelrnd 6962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑥) ∈ 𝑃)
257		simp-8r 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ 𝐵)
258	254, 257	ffvelrnd 6962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑦) ∈ 𝑃)
259		simp-7r 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑧 ∈ 𝐵)
260	254, 259	ffvelrnd 6962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑧) ∈ 𝑃)
261		simp-5r 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑎 ∈ 𝐵)
262	254, 261	ffvelrnd 6962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑎) ∈ 𝑃)
263		simp-4r 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ 𝐵)
264	254, 263	ffvelrnd 6962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑏) ∈ 𝑃)
265		simpllr 773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑐 ∈ 𝐵)
266	254, 265	ffvelrnd 6962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑐) ∈ 𝑃)
267		simp-6r 785	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑢 ∈ 𝐵)
268	254, 267	ffvelrnd 6962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑢) ∈ 𝑃)
269		simplr 766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑣 ∈ 𝐵)
270	254, 269	ffvelrnd 6962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑣) ∈ 𝑃)
271	8	ad9antr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵–1-1-onto→𝑃)
272	271, 255	jca 512	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵))
273		simprl1 1217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥 ≠ 𝑦)
274		dff1o6 7147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐵–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
275	274	simp3bi 1146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
276	275	r19.21bi 3134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
277	276	r19.21bi 3134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
278	277	necon3d 2964	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑥 ≠ 𝑦 → (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
279	278	imp 407	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ≠ 𝑦) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
280	272, 257, 273, 279	syl21anc 835	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
281		simprl2 1218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ (𝑥𝐽𝑧))
282	21	ex 413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))))
283	282	ad9antr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))))
284	283	imp 407	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
285	23	ex 413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))))
286	285	ad9antr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))))
287	286	imp 407	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
288	3, 4, 5, 17, 18, 19, 271, 284, 287, 255, 259, 257	f1otrgitv 27231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧))))
289	281, 288	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧)))
290		simprl3 1219	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ (𝑎𝐽𝑐))
291	3, 4, 5, 17, 18, 19, 271, 284, 287, 261, 265, 263	f1otrgitv 27231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏 ∈ (𝑎𝐽𝑐) ↔ (𝐹‘𝑏) ∈ ((𝐹‘𝑎)𝐼(𝐹‘𝑐))))
292	290, 291	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑏) ∈ ((𝐹‘𝑎)𝐼(𝐹‘𝑐)))
293		simprr 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))
294	293	simpld 495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)))
295	294	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = (𝑎𝐸𝑏))
296	3, 4, 5, 17, 18, 19, 271, 284, 287, 255, 257	f1otrgds 27230	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = ((𝐹‘𝑥)𝐷(𝐹‘𝑦)))
297	3, 4, 5, 17, 18, 19, 271, 284, 287, 261, 263	f1otrgds 27230	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑏) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))
298	295, 296, 297	3eqtr3d 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))
299	294	simprd 496	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = (𝑏𝐸𝑐))
300	3, 4, 5, 17, 18, 19, 271, 284, 287, 257, 259	f1otrgds 27230	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = ((𝐹‘𝑦)𝐷(𝐹‘𝑧)))
301	3, 4, 5, 17, 18, 19, 271, 284, 287, 263, 265	f1otrgds 27230	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑐) = ((𝐹‘𝑏)𝐷(𝐹‘𝑐)))
302	299, 300, 301	3eqtr3d 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑦)𝐷(𝐹‘𝑧)) = ((𝐹‘𝑏)𝐷(𝐹‘𝑐)))
303	293	simprd 496	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))
304	303	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = (𝑎𝐸𝑣))
305	3, 4, 5, 17, 18, 19, 271, 284, 287, 255, 267	f1otrgds 27230	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = ((𝐹‘𝑥)𝐷(𝐹‘𝑢)))
306	3, 4, 5, 17, 18, 19, 271, 284, 287, 261, 269	f1otrgds 27230	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑣) = ((𝐹‘𝑎)𝐷(𝐹‘𝑣)))
307	304, 305, 306	3eqtr3d 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑥)𝐷(𝐹‘𝑢)) = ((𝐹‘𝑎)𝐷(𝐹‘𝑣)))
308	303	simprd 496	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = (𝑏𝐸𝑣))
309	3, 4, 5, 17, 18, 19, 271, 284, 287, 257, 267	f1otrgds 27230	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = ((𝐹‘𝑦)𝐷(𝐹‘𝑢)))
310	3, 4, 5, 17, 18, 19, 271, 284, 287, 263, 269	f1otrgds 27230	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑣) = ((𝐹‘𝑏)𝐷(𝐹‘𝑣)))
311	308, 309, 310	3eqtr3d 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑦)𝐷(𝐹‘𝑢)) = ((𝐹‘𝑏)𝐷(𝐹‘𝑣)))
312	3, 4, 5, 253, 256, 258, 260, 262, 264, 266, 268, 270, 280, 289, 292, 298, 302, 307, 311	axtg5seg 26826	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑧)𝐷(𝐹‘𝑢)) = ((𝐹‘𝑐)𝐷(𝐹‘𝑣)))
313	3, 4, 5, 17, 18, 19, 271, 284, 287, 259, 267	f1otrgds 27230	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = ((𝐹‘𝑧)𝐷(𝐹‘𝑢)))
314	3, 4, 5, 17, 18, 19, 271, 284, 287, 265, 269	f1otrgds 27230	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑐𝐸𝑣) = ((𝐹‘𝑐)𝐷(𝐹‘𝑣)))
315	312, 313, 314	3eqtr4d 2788	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))
316	315	ex 413	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) → (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
317	316	ralrimiva 3103	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
318	317	ralrimiva 3103	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
319	318	ralrimiva 3103	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
320	319	ralrimiva 3103	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
321	320	ralrimiva 3103	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
322	321	ralrimiva 3103	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
323	322	ralrimiva 3103	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
324	323	ralrimiva 3103	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
325		simp-4l 780	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝜑)
326		simplr 766	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑤 ∈ 𝑃)
327		simprl 768	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤))
328	325, 8	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝐹:𝐵–1-1-onto→𝑃)
329		f1ocnvfv2 7149	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑤 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑤)) = 𝑤)
330	328, 326, 329	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝐹‘(^◡𝐹‘𝑤)) = 𝑤)
331	330	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑤))) = ((𝐹‘𝑥)𝐼𝑤))
332	327, 331	eleqtrrd 2842	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑤))))
333	325, 21	sylan 580	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
334	325, 23	sylan 580	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
335	12	ad3antrrr 727	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑥 ∈ 𝐵)
336	76	ffvelrnda 6961	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑃) → (^◡𝐹‘𝑤) ∈ 𝐵)
337	325, 326, 336	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (^◡𝐹‘𝑤) ∈ 𝐵)
338	14	ad3antrrr 727	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑦 ∈ 𝐵)
339	3, 4, 5, 17, 18, 19, 328, 333, 334, 335, 337, 338	f1otrgitv 27231	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑤)) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑤)))))
340	332, 339	mpbird 256	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑤)))
341	3, 4, 5, 17, 18, 19, 328, 333, 334, 338, 337	f1otrgds 27230	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦𝐸(^◡𝐹‘𝑤)) = ((𝐹‘𝑦)𝐷(𝐹‘(^◡𝐹‘𝑤))))
342	330	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ((𝐹‘𝑦)𝐷(𝐹‘(^◡𝐹‘𝑤))) = ((𝐹‘𝑦)𝐷𝑤))
343		simprr 770	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))
344	341, 342, 343	3eqtrd 2782	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦𝐸(^◡𝐹‘𝑤)) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))
345		simprl 768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵)
346	345	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑎 ∈ 𝐵)
347		simprr 770	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵)
348	347	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑏 ∈ 𝐵)
349	3, 4, 5, 17, 18, 19, 328, 333, 334, 346, 348	f1otrgds 27230	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑎𝐸𝑏) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))
350	344, 349	eqtr4d 2781	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦𝐸(^◡𝐹‘𝑤)) = (𝑎𝐸𝑏))
351		oveq2 7283	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (^◡𝐹‘𝑤) → (𝑥𝐽𝑧) = (𝑥𝐽(^◡𝐹‘𝑤)))
352	351	eleq2d 2824	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (^◡𝐹‘𝑤) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑤))))
353		oveq2 7283	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (^◡𝐹‘𝑤) → (𝑦𝐸𝑧) = (𝑦𝐸(^◡𝐹‘𝑤)))
354	353	eqeq1d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (^◡𝐹‘𝑤) → ((𝑦𝐸𝑧) = (𝑎𝐸𝑏) ↔ (𝑦𝐸(^◡𝐹‘𝑤)) = (𝑎𝐸𝑏)))
355	352, 354	anbi12d 631	. . . . . . . . . . . . 13 ⊢ (𝑧 = (^◡𝐹‘𝑤) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑤)) ∧ (𝑦𝐸(^◡𝐹‘𝑤)) = (𝑎𝐸𝑏))))
356	355	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑃) ∧ 𝑧 = (^◡𝐹‘𝑤)) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑤)) ∧ (𝑦𝐸(^◡𝐹‘𝑤)) = (𝑎𝐸𝑏))))
357	336, 356	rspcedv 3554	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑃) → ((𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑤)) ∧ (𝑦𝐸(^◡𝐹‘𝑤)) = (𝑎𝐸𝑏)) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))
358	357	imp 407	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑃) ∧ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑤)) ∧ (𝑦𝐸(^◡𝐹‘𝑤)) = (𝑎𝐸𝑏))) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
359	325, 326, 340, 350, 358	syl22anc 836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
360	7	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐺 ∈ TarskiG)
361	13	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃)
362	15	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃)
363	11	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃)
364	363, 345	ffvelrnd 6962	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑎) ∈ 𝑃)
365	363, 347	ffvelrnd 6962	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑏) ∈ 𝑃)
366	3, 4, 5, 360, 361, 362, 364, 365	axtgsegcon 26825	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑤 ∈ 𝑃 ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))))
367	359, 366	r19.29a 3218	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
368	367	ralrimivva 3123	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
369	368	ralrimivva 3123	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
370	2, 324, 369	jca32 516	. . . . 5 ⊢ (𝜑 → (𝐻 ∈ V ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
371	17, 18, 19	istrkgcb 26817	. . . . 5 ⊢ (𝐻 ∈ TarskiG_CB ↔ (𝐻 ∈ V ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
372	370, 371	sylibr 233	. . . 4 ⊢ (𝜑 → 𝐻 ∈ TarskiG_CB)
373		f1otrg.l	. . . . 5 ⊢ (𝜑 → (LineG‘𝐻) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))
374	17, 18, 19	istrkgl 26819	. . . . 5 ⊢ (𝐻 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineG‘𝐻) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))})))
375	2, 373, 374	sylanbrc 583	. . . 4 ⊢ (𝜑 → 𝐻 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
376	372, 375	elind 4128	. . 3 ⊢ (𝜑 → 𝐻 ∈ (TarskiG_CB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
377	252, 376	elind 4128	. 2 ⊢ (𝜑 → 𝐻 ∈ ((TarskiG_C ∩ TarskiG_B) ∩ (TarskiG_CB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})))
378		df-trkg 26814	. 2 ⊢ TarskiG = ((TarskiG_C ∩ TarskiG_B) ∩ (TarskiG_CB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
379	377, 378	eleqtrrdi 2850	1 ⊢ (𝜑 → 𝐻 ∈ TarskiG)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∨ w3o 1085 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 {cab 2715 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 {crab 3068 Vcvv 3432 [wsbc 3716 ∖ cdif 3884 ∩ cin 3886 ⊆ wss 3887 𝒫 cpw 4533 {csn 4561 ^◡ccnv 5588 ran crn 5590 “ cima 5592 Fn wfn 6428 ⟶wf 6429 –1-1→wf1 6430 –onto→wfo 6431 –1-1-onto→wf1o 6432 ‘cfv 6433 (class class class)co 7275 ∈ cmpo 7277 Basecbs 16912 distcds 16971 TarskiGcstrkg 26788 TarskiG_Ccstrkgc 26789 TarskiG_Bcstrkgb 26790 TarskiG_CBcstrkgcb 26791 Itvcitv 26794 LineGclng 26795

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-pr 5352

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-rab 3073 df-v 3434 df-sbc 3717 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-id 5489 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-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-trkgc 26809 df-trkgb 26810 df-trkgcb 26811 df-trkg 26814

This theorem is referenced by: (None)

W3C validator