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

Theorem f1otrg 26042
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.
StepHypRef Expression
1 f1otrg.h . . . . . 6 (𝜑𝐻𝑉)
2 elex 3365 . . . . . 6 (𝐻𝑉𝐻 ∈ V)
31, 2syl 17 . . . . 5 (𝜑𝐻 ∈ V)
4 f1otrkg.p . . . . . . . . 9 𝑃 = (Base‘𝐺)
5 f1otrkg.d . . . . . . . . 9 𝐷 = (dist‘𝐺)
6 f1otrkg.i . . . . . . . . 9 𝐼 = (Itv‘𝐺)
7 f1otrg.g . . . . . . . . . 10 (𝜑𝐺 ∈ TarskiG)
87adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐺 ∈ TarskiG)
9 f1otrkg.f . . . . . . . . . . . 12 (𝜑𝐹:𝐵1-1-onto𝑃)
10 f1of 6320 . . . . . . . . . . . 12 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵𝑃)
119, 10syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝑃)
1211adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹:𝐵𝑃)
13 simprl 787 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
1412, 13ffvelrnd 6550 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑥) ∈ 𝑃)
15 simprr 789 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
1612, 15ffvelrnd 6550 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑦) ∈ 𝑃)
174, 5, 6, 8, 14, 16axtgcgrrflx 25652 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑦)𝐷(𝐹𝑥)))
18 f1otrkg.b . . . . . . . . 9 𝐵 = (Base‘𝐻)
19 f1otrkg.e . . . . . . . . 9 𝐸 = (dist‘𝐻)
20 f1otrkg.j . . . . . . . . 9 𝐽 = (Itv‘𝐻)
219adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹:𝐵1-1-onto𝑃)
22 f1otrkg.1 . . . . . . . . . 10 ((𝜑 ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
2322adantlr 706 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
24 f1otrkg.2 . . . . . . . . . 10 ((𝜑 ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2524adantlr 706 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
264, 5, 6, 18, 19, 20, 21, 23, 25, 13, 15f1otrgds 26040 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
274, 5, 6, 18, 19, 20, 21, 23, 25, 15, 13f1otrgds 26040 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦𝐸𝑥) = ((𝐹𝑦)𝐷(𝐹𝑥)))
2817, 26, 273eqtr4d 2809 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
2928ralrimivva 3118 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
30 f1of1 6319 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵1-1𝑃)
319, 30syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵1-1𝑃)
32313ad2ant1 1163 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1𝑃)
33 simp21 1263 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥𝐵)
34 simp22 1264 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑦𝐵)
3533, 34jca 507 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐵𝑦𝐵))
3673ad2ant1 1163 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐺 ∈ TarskiG)
37113ad2ant1 1163 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵𝑃)
3837, 33ffvelrnd 6550 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) ∈ 𝑃)
3937, 34ffvelrnd 6550 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑦) ∈ 𝑃)
40 simp23 1265 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑧𝐵)
4137, 40ffvelrnd 6550 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑧) ∈ 𝑃)
42 simp3 1168 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = (𝑧𝐸𝑧))
4393ad2ant1 1163 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1-onto𝑃)
44223ad2antl1 1236 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
45243ad2antl1 1236 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
464, 5, 6, 18, 19, 20, 43, 44, 45, 33, 34f1otrgds 26040 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
474, 5, 6, 18, 19, 20, 43, 44, 45, 40, 40f1otrgds 26040 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑧𝐸𝑧) = ((𝐹𝑧)𝐷(𝐹𝑧)))
4842, 46, 473eqtr3d 2807 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑧)𝐷(𝐹𝑧)))
494, 5, 6, 36, 38, 39, 41, 48axtgcgrid 25653 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) = (𝐹𝑦))
50 f1veqaeq 6706 . . . . . . . . . 10 ((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
5150imp 395 . . . . . . . . 9 (((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
5232, 35, 49, 51syl21anc 866 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 = 𝑦)
53523expia 1150 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5453ralrimivvva 3119 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5529, 54jca 507 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)))
5618, 19, 20istrkgc 25644 . . . . 5 (𝐻 ∈ TarskiGC ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))))
573, 55, 56sylanbrc 578 . . . 4 (𝜑𝐻 ∈ TarskiGC)
5893ad2ant1 1163 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1-onto𝑃)
5958, 30syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1𝑃)
60 simp2 1167 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑥𝐵𝑦𝐵))
6173ad2ant1 1163 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐺 ∈ TarskiG)
62143adant3 1162 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) ∈ 𝑃)
63163adant3 1162 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ 𝑃)
64 simp3 1168 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ (𝑥𝐽𝑥))
65223ad2antl1 1236 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
66243ad2antl1 1236 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
67133adant3 1162 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥𝐵)
68153adant3 1162 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦𝐵)
694, 5, 6, 18, 19, 20, 58, 65, 66, 67, 67, 68f1otrgitv 26041 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑦 ∈ (𝑥𝐽𝑥) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥))))
7064, 69mpbid 223 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥)))
714, 5, 6, 61, 62, 63, 70axtgbtwnid 25656 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) = (𝐹𝑦))
7259, 60, 71, 51syl21anc 866 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 = 𝑦)
73723expia 1150 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
7473ralrimivva 3118 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
75 f1ocnv 6332 . . . . . . . . . . . . . 14 (𝐹:𝐵1-1-onto𝑃𝐹:𝑃1-1-onto𝐵)
76 f1of 6320 . . . . . . . . . . . . . 14 (𝐹:𝑃1-1-onto𝐵𝐹:𝑃𝐵)
779, 75, 763syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝑃𝐵)
7877ad5antr 728 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝑃𝐵)
79 simplr 785 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐𝑃)
8078, 79ffvelrnd 6550 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ 𝐵)
81 simpr 477 . . . . . . . . . . . . 13 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → 𝑎 = (𝐹𝑐))
8281eleq1d 2829 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑢𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑢𝐽𝑦)))
8381eleq1d 2829 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑣𝐽𝑥) ↔ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
8482, 83anbi12d 624 . . . . . . . . . . 11 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → ((𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)) ↔ ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥))))
85 simprl 787 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
8621ad2antrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵1-1-onto𝑃)
8786ad2antrr 717 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝐵1-1-onto𝑃)
88 f1ocnvfv2 6725 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → (𝐹‘(𝐹𝑐)) = 𝑐)
8988eleq1d 2829 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
9087, 79, 89syl2anc 579 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
9185, 90mpbird 248 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
92 simplll 791 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵)) → (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))))
93 simplll 791 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵)) → (𝜑 ∧ (𝑥𝐵𝑦𝐵)))
9493, 23sylancom 582 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
9592, 94sylancom 582 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
96 simplll 791 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))))
97 simplll 791 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝜑 ∧ (𝑥𝐵𝑦𝐵)))
9897, 25sylancom 582 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
9996, 98sylancom 582 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
100 simplr2 1277 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢𝐵)
101100ad2antrr 717 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑢𝐵)
10215ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑦𝐵)
103102ad2antrr 717 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑦𝐵)
1044, 5, 6, 18, 19, 20, 87, 95, 99, 101, 103, 80f1otrgitv 26041 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
10591, 104mpbird 248 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑢𝐽𝑦))
106 simprr 789 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
10788eleq1d 2829 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
10887, 79, 107syl2anc 579 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
109106, 108mpbird 248 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
110 simplr3 1279 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣𝐵)
111110ad2antrr 717 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑣𝐵)
11213ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑥𝐵)
113112ad2antrr 717 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑥𝐵)
1144, 5, 6, 18, 19, 20, 87, 95, 99, 111, 113, 80f1otrgitv 26041 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑣𝐽𝑥) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
115109, 114mpbird 248 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑣𝐽𝑥))
116105, 115jca 507 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
11780, 84, 116rspcedvd 3468 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
1188ad2antrr 717 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐺 ∈ TarskiG)
11912ad2antrr 717 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵𝑃)
120119, 112ffvelrnd 6550 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑥) ∈ 𝑃)
121119, 102ffvelrnd 6550 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑦) ∈ 𝑃)
122 simplr1 1275 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑧𝐵)
123119, 122ffvelrnd 6550 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑧) ∈ 𝑃)
124119, 100ffvelrnd 6550 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ 𝑃)
125119, 110ffvelrnd 6550 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ 𝑃)
126 simprl 787 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ (𝑥𝐽𝑧))
1274, 5, 6, 18, 19, 20, 86, 94, 98, 112, 122, 100f1otrgitv 26041 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑢 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
128126, 127mpbid 223 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
129 simprr 789 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ (𝑦𝐽𝑧))
1304, 5, 6, 18, 19, 20, 86, 94, 98, 102, 122, 110f1otrgitv 26041 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑣 ∈ (𝑦𝐽𝑧) ↔ (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧))))
131129, 130mpbid 223 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧)))
1324, 5, 6, 118, 120, 121, 123, 124, 125, 128, 131axtgpasch 25657 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑐𝑃 (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
133117, 132r19.29a 3225 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
134133ex 401 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
135134ralrimivvva 3119 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
136135ralrimivva 3118 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
1379ad5antr 728 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
138 simpllr 793 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
139137, 138, 88syl2anc 579 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) = 𝑐)
140 ffn 6223 . . . . . . . . . . . . . . . . . 18 (𝐹:𝐵𝑃𝐹 Fn 𝐵)
141137, 10, 1403syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹 Fn 𝐵)
142 simp-4r 803 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
143142simpld 488 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠 ∈ 𝒫 𝐵)
144143elpwid 4327 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
145144adantlr 706 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
146 simprl 787 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
147 fnfvima 6689 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝐵𝑠𝐵𝑥𝑠) → (𝐹𝑥) ∈ (𝐹𝑠))
148141, 145, 146, 147syl3anc 1490 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑥) ∈ (𝐹𝑠))
149142simprd 489 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡 ∈ 𝒫 𝐵)
150149elpwid 4327 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
151150adantlr 706 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
152 simprr 789 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
153 fnfvima 6689 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝐵𝑡𝐵𝑦𝑡) → (𝐹𝑦) ∈ (𝐹𝑡))
154141, 151, 152, 153syl3anc 1490 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑦) ∈ (𝐹𝑡))
155 simplr 785 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
156 oveq1 6849 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝐹𝑥) → (𝑒𝐼𝑓) = ((𝐹𝑥)𝐼𝑓))
157156eleq2d 2830 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝐹𝑥) → (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼𝑓)))
158 oveq2 6850 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝐹𝑦) → ((𝐹𝑥)𝐼𝑓) = ((𝐹𝑥)𝐼(𝐹𝑦)))
159158eleq2d 2830 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝐹𝑦) → (𝑐 ∈ ((𝐹𝑥)𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
160157, 159rspc2va 3475 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∈ (𝐹𝑠) ∧ (𝐹𝑦) ∈ (𝐹𝑡)) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
161148, 154, 155, 160syl21anc 866 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
162139, 161eqeltrd 2844 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
1639ad4antr 724 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
164 simp-5l 805 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
165164, 22sylancom 582 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
166 simp-5l 805 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
167166, 24sylancom 582 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
168 simprl 787 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
169144, 168sseldd 3762 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝐵)
170 simprr 789 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
171150, 170sseldd 3762 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝐵)
17277ad4antr 724 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝑃𝐵)
173 simplr 785 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
174172, 173ffvelrnd 6550 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ 𝐵)
1754, 5, 6, 18, 19, 20, 163, 165, 167, 169, 171, 174f1otrgitv 26041 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
176175adantlr 706 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
177162, 176mpbird 248 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ (𝑥𝐽𝑦))
178177ralrimivva 3118 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
179178adantllr 710 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
18077ad4antr 724 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝐹:𝑃𝐵)
181 simpr 477 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝑐𝑃)
182180, 181ffvelrnd 6550 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (𝐹𝑐) ∈ 𝐵)
183 eleq1 2832 . . . . . . . . . . . . . . 15 (𝑏 = (𝐹𝑐) → (𝑏 ∈ (𝑥𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
1841832ralbidv 3136 . . . . . . . . . . . . . 14 (𝑏 = (𝐹𝑐) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
185184adantl 473 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ 𝑏 = (𝐹𝑐)) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
186182, 185rspcedv 3465 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
187186adantr 472 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
188179, 187mpd 15 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
1897ad3antrrr 721 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐺 ∈ TarskiG)
190 imassrn 5659 . . . . . . . . . . . 12 (𝐹𝑠) ⊆ ran 𝐹
191 f1ofo 6327 . . . . . . . . . . . . . 14 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵onto𝑃)
192 forn 6301 . . . . . . . . . . . . . 14 (𝐹:𝐵onto𝑃 → ran 𝐹 = 𝑃)
1939, 191, 1923syl 18 . . . . . . . . . . . . 13 (𝜑 → ran 𝐹 = 𝑃)
194193ad3antrrr 721 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ran 𝐹 = 𝑃)
195190, 194syl5sseq 3813 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑠) ⊆ 𝑃)
196 imassrn 5659 . . . . . . . . . . . 12 (𝐹𝑡) ⊆ ran 𝐹
197196, 194syl5sseq 3813 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑡) ⊆ 𝑃)
19811ad3antrrr 721 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐹:𝐵𝑃)
199 simplr 785 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝑎𝐵)
200198, 199ffvelrnd 6550 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑎) ∈ 𝑃)
2019ad5antr 728 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1-onto𝑃)
202 ffn 6223 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑃𝐵𝐹 Fn 𝑃)
203201, 75, 76, 2024syl 19 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹 Fn 𝑃)
204195ad2antrr 717 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑠) ⊆ 𝑃)
205 simplr 785 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ (𝐹𝑠))
206 fnfvima 6689 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑃 ∧ (𝐹𝑠) ⊆ 𝑃𝑢 ∈ (𝐹𝑠)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
207203, 204, 205, 206syl3anc 1490 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
208201, 30syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1𝑃)
209 simp-5r 807 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
210209simpld 488 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠 ∈ 𝒫 𝐵)
211210elpwid 4327 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠𝐵)
212 f1imacnv 6336 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐵1-1𝑃𝑠𝐵) → (𝐹 “ (𝐹𝑠)) = 𝑠)
213208, 211, 212syl2anc 579 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑠)) = 𝑠)
214207, 213eleqtrd 2846 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝑠)
215197ad2antrr 717 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑡) ⊆ 𝑃)
216 simpr 477 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣 ∈ (𝐹𝑡))
217 fnfvima 6689 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑃 ∧ (𝐹𝑡) ⊆ 𝑃𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
218203, 215, 216, 217syl3anc 1490 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
219209simprd 489 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡 ∈ 𝒫 𝐵)
220219elpwid 4327 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡𝐵)
221 f1imacnv 6336 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐵1-1𝑃𝑡𝐵) → (𝐹 “ (𝐹𝑡)) = 𝑡)
222208, 220, 221syl2anc 579 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑡)) = 𝑡)
223218, 222eleqtrd 2846 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝑡)
224 simpllr 793 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦))
225 eleq1 2832 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐹𝑢) → (𝑥 ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽𝑦)))
226 oveq2 6850 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐹𝑣) → (𝑎𝐽𝑦) = (𝑎𝐽(𝐹𝑣)))
227226eleq2d 2830 . . . . . . . . . . . . . . . 16 (𝑦 = (𝐹𝑣) → ((𝐹𝑢) ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣))))
228225, 227rspc2va 3475 . . . . . . . . . . . . . . 15 ((((𝐹𝑢) ∈ 𝑠 ∧ (𝐹𝑣) ∈ 𝑡) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
229214, 223, 224, 228syl21anc 866 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
230 simp-6l 809 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
231230, 22sylancom 582 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
232 simp-6l 809 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
233232, 24sylancom 582 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
234 simp-4r 803 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑎𝐵)
235215, 216sseldd 3762 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣𝑃)
236 f1ocnvdm 6732 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹𝑣) ∈ 𝐵)
237201, 235, 236syl2anc 579 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝐵)
238204, 205sseldd 3762 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢𝑃)
239 f1ocnvdm 6732 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹𝑢) ∈ 𝐵)
240201, 238, 239syl2anc 579 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝐵)
2414, 5, 6, 18, 19, 20, 201, 231, 233, 234, 237, 240f1otrgitv 26041 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)) ↔ (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣)))))
242229, 241mpbid 223 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))))
243 f1ocnvfv2 6725 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹‘(𝐹𝑢)) = 𝑢)
244201, 238, 243syl2anc 579 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) = 𝑢)
245 f1ocnvfv2 6725 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹‘(𝐹𝑣)) = 𝑣)
246201, 235, 245syl2anc 579 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑣)) = 𝑣)
247246oveq2d 6858 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))) = ((𝐹𝑎)𝐼𝑣))
248242, 244, 2473eltr3d 2858 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2492483impa 1136 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2504, 5, 6, 189, 195, 197, 200, 249axtgcont 25659 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑐𝑃𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
251188, 250r19.29a 3225 . . . . . . . . 9 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
252251r19.29an 3224 . . . . . . . 8 (((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ ∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
253252ex 401 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
254253ralrimivva 3118 . . . . . 6 (𝜑 → ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
25574, 136, 2543jca 1158 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))))
25618, 19, 20istrkgb 25645 . . . . 5 (𝐻 ∈ TarskiGB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))))
2573, 255, 256sylanbrc 578 . . . 4 (𝜑𝐻 ∈ TarskiGB)
25857, 257elind 3960 . . 3 (𝜑𝐻 ∈ (TarskiGC ∩ TarskiGB))
2597ad9antr 744 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐺 ∈ TarskiG)
26011ad9antr 744 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵𝑃)
261 simp-9r 823 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝐵)
262260, 261ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ∈ 𝑃)
263 simp-8r 819 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦𝐵)
264260, 263ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ 𝑃)
265 simp-7r 815 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑧𝐵)
266260, 265ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑧) ∈ 𝑃)
267 simp-5r 807 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑎𝐵)
268260, 267ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑎) ∈ 𝑃)
269 simp-4r 803 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏𝐵)
270260, 269ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ 𝑃)
271 simpllr 793 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑐𝐵)
272260, 271ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑐) ∈ 𝑃)
273 simp-6r 811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑢𝐵)
274260, 273ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑢) ∈ 𝑃)
275 simplr 785 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑣𝐵)
276260, 275ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑣) ∈ 𝑃)
2779ad9antr 744 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵1-1-onto𝑃)
278277, 261jca 507 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹:𝐵1-1-onto𝑃𝑥𝐵))
279 simprl1 1281 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝑦)
280 dff1o6 6723 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
281280simp3bi 1177 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝐵1-1-onto𝑃 → ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
282281r19.21bi 3079 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐵1-1-onto𝑃𝑥𝐵) → ∀𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
283282r19.21bi 3079 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
284283necon3d 2958 . . . . . . . . . . . . . . . . . . 19 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → (𝑥𝑦 → (𝐹𝑥) ≠ (𝐹𝑦)))
285284imp 395 . . . . . . . . . . . . . . . . . 18 ((((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝑦) → (𝐹𝑥) ≠ (𝐹𝑦))
286278, 263, 279, 285syl21anc 866 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ≠ (𝐹𝑦))
287 simprl2 1283 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ (𝑥𝐽𝑧))
28822ex 401 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
289288ad9antr 744 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
290289imp 395 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
29124ex 401 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
292291ad9antr 744 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
293292imp 395 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2944, 5, 6, 18, 19, 20, 277, 290, 293, 261, 265, 263f1otrgitv 26041 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
295287, 294mpbid 223 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
296 simprl3 1285 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ (𝑎𝐽𝑐))
2974, 5, 6, 18, 19, 20, 277, 290, 293, 267, 271, 269f1otrgitv 26041 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏 ∈ (𝑎𝐽𝑐) ↔ (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐))))
298296, 297mpbid 223 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐)))
299 simprr 789 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))
300299simpld 488 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)))
301300simpld 488 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = (𝑎𝐸𝑏))
3024, 5, 6, 18, 19, 20, 277, 290, 293, 261, 263f1otrgds 26040 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
3034, 5, 6, 18, 19, 20, 277, 290, 293, 267, 269f1otrgds 26040 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
304301, 302, 3033eqtr3d 2807 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
305300simprd 489 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = (𝑏𝐸𝑐))
3064, 5, 6, 18, 19, 20, 277, 290, 293, 263, 265f1otrgds 26040 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = ((𝐹𝑦)𝐷(𝐹𝑧)))
3074, 5, 6, 18, 19, 20, 277, 290, 293, 269, 271f1otrgds 26040 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑐) = ((𝐹𝑏)𝐷(𝐹𝑐)))
308305, 306, 3073eqtr3d 2807 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑧)) = ((𝐹𝑏)𝐷(𝐹𝑐)))
309299simprd 489 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))
310309simpld 488 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = (𝑎𝐸𝑣))
3114, 5, 6, 18, 19, 20, 277, 290, 293, 261, 273f1otrgds 26040 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = ((𝐹𝑥)𝐷(𝐹𝑢)))
3124, 5, 6, 18, 19, 20, 277, 290, 293, 267, 275f1otrgds 26040 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑣) = ((𝐹𝑎)𝐷(𝐹𝑣)))
313310, 311, 3123eqtr3d 2807 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑢)) = ((𝐹𝑎)𝐷(𝐹𝑣)))
314309simprd 489 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = (𝑏𝐸𝑣))
3154, 5, 6, 18, 19, 20, 277, 290, 293, 263, 273f1otrgds 26040 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = ((𝐹𝑦)𝐷(𝐹𝑢)))
3164, 5, 6, 18, 19, 20, 277, 290, 293, 269, 275f1otrgds 26040 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑣) = ((𝐹𝑏)𝐷(𝐹𝑣)))
317314, 315, 3163eqtr3d 2807 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑢)) = ((𝐹𝑏)𝐷(𝐹𝑣)))
3184, 5, 6, 259, 262, 264, 266, 268, 270, 272, 274, 276, 286, 295, 298, 304, 308, 313, 317axtg5seg 25655 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑧)𝐷(𝐹𝑢)) = ((𝐹𝑐)𝐷(𝐹𝑣)))
3194, 5, 6, 18, 19, 20, 277, 290, 293, 265, 273f1otrgds 26040 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = ((𝐹𝑧)𝐷(𝐹𝑢)))
3204, 5, 6, 18, 19, 20, 277, 290, 293, 271, 275f1otrgds 26040 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑐𝐸𝑣) = ((𝐹𝑐)𝐷(𝐹𝑣)))
321318, 319, 3203eqtr4d 2809 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))
322321ex 401 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) → (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
323322ralrimiva 3113 . . . . . . . . . . . . 13 ((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) → ∀𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
324323ralrimiva 3113 . . . . . . . . . . . 12 (((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) → ∀𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
325324ralrimiva 3113 . . . . . . . . . . 11 ((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) → ∀𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
326325ralrimiva 3113 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) → ∀𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
327326ralrimiva 3113 . . . . . . . . 9 ((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) → ∀𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
328327ralrimiva 3113 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → ∀𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
329328ralrimiva 3113 . . . . . . 7 ((𝜑𝑥𝐵) → ∀𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
330329ralrimiva 3113 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
331 simp-4l 801 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝜑)
332 simplr 785 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑤𝑃)
333 simprl 787 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤))
334331, 9syl 17 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝐹:𝐵1-1-onto𝑃)
335 f1ocnvfv2 6725 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑤𝑃) → (𝐹‘(𝐹𝑤)) = 𝑤)
336334, 332, 335syl2anc 579 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹‘(𝐹𝑤)) = 𝑤)
337336oveq2d 6858 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))) = ((𝐹𝑥)𝐼𝑤))
338333, 337eleqtrrd 2847 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))))
339331, 22sylan 575 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
340331, 24sylan 575 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
34113ad3antrrr 721 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑥𝐵)
34277ffvelrnda 6549 . . . . . . . . . . . . 13 ((𝜑𝑤𝑃) → (𝐹𝑤) ∈ 𝐵)
343331, 332, 342syl2anc 579 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑤) ∈ 𝐵)
34415ad3antrrr 721 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦𝐵)
3454, 5, 6, 18, 19, 20, 334, 339, 340, 341, 343, 344f1otrgitv 26041 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤)))))
346338, 345mpbird 248 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦 ∈ (𝑥𝐽(𝐹𝑤)))
3474, 5, 6, 18, 19, 20, 334, 339, 340, 344, 343f1otrgds 26040 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))))
348336oveq2d 6858 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))) = ((𝐹𝑦)𝐷𝑤))
349 simprr 789 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))
350347, 348, 3493eqtrd 2803 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
351 simprl 787 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑎𝐵)
352351ad2antrr 717 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑎𝐵)
353 simprr 789 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑏𝐵)
354353ad2antrr 717 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑏𝐵)
3554, 5, 6, 18, 19, 20, 334, 339, 340, 352, 354f1otrgds 26040 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
356350, 355eqtr4d 2802 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))
357 oveq2 6850 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑥𝐽𝑧) = (𝑥𝐽(𝐹𝑤)))
358357eleq2d 2830 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ 𝑦 ∈ (𝑥𝐽(𝐹𝑤))))
359 oveq2 6850 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑦𝐸𝑧) = (𝑦𝐸(𝐹𝑤)))
360359eqeq1d 2767 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → ((𝑦𝐸𝑧) = (𝑎𝐸𝑏) ↔ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)))
361358, 360anbi12d 624 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑤) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
362361adantl 473 . . . . . . . . . . . 12 (((𝜑𝑤𝑃) ∧ 𝑧 = (𝐹𝑤)) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
363342, 362rspcedv 3465 . . . . . . . . . . 11 ((𝜑𝑤𝑃) → ((𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))
364363imp 395 . . . . . . . . . 10 (((𝜑𝑤𝑃) ∧ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
365331, 332, 346, 356, 364syl22anc 867 . . . . . . . . 9 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3668adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐺 ∈ TarskiG)
36714adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑥) ∈ 𝑃)
36816adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑦) ∈ 𝑃)
36912adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐹:𝐵𝑃)
370369, 351ffvelrnd 6550 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑎) ∈ 𝑃)
371369, 353ffvelrnd 6550 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑏) ∈ 𝑃)
3724, 5, 6, 366, 367, 368, 370, 371axtgsegcon 25654 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑤𝑃 ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏))))
373365, 372r19.29a 3225 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
374373ralrimivva 3118 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
375374ralrimivva 3118 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3763, 330, 375jca32 511 . . . . 5 (𝜑 → (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
37718, 19, 20istrkgcb 25646 . . . . 5 (𝐻 ∈ TarskiGCB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
378376, 377sylibr 225 . . . 4 (𝜑𝐻 ∈ TarskiGCB)
379 f1otrg.l . . . . 5 (𝜑 → (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))
38018, 19, 20istrkgl 25648 . . . . 5 (𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))})))
3813, 379, 380sylanbrc 578 . . . 4 (𝜑𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
382378, 381elind 3960 . . 3 (𝜑𝐻 ∈ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
383258, 382elind 3960 . 2 (𝜑𝐻 ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})))
384 df-trkg 25643 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
385383, 384syl6eleqr 2855 1 (𝜑𝐻 ∈ TarskiG)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3o 1106  w3a 1107   = wceq 1652  wcel 2155  {cab 2751  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  [wsbc 3596  cdif 3729  cin 3731  wss 3732  𝒫 cpw 4315  {csn 4334  ccnv 5276  ran crn 5278  cima 5280   Fn wfn 6063  wf 6064  1-1wf1 6065  ontowfo 6066  1-1-ontowf1o 6067  cfv 6068  (class class class)co 6842  cmpt2 6844  Basecbs 16130  distcds 16223  TarskiGcstrkg 25620  TarskiGCcstrkgc 25621  TarskiGBcstrkgb 25622  TarskiGCBcstrkgcb 25623  Itvcitv 25626  LineGclng 25627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-trkgc 25638  df-trkgb 25639  df-trkgcb 25640  df-trkg 25643
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator