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

Theorem f1otrg 25950
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 3352 . . . . . 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 6298 . . . . . . . . . . . 12 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵𝑃)
119, 10syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝑃)
1211adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹:𝐵𝑃)
13 simprl 811 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
1412, 13ffvelrnd 6523 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑥) ∈ 𝑃)
15 simprr 813 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
1612, 15ffvelrnd 6523 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑦) ∈ 𝑃)
174, 5, 6, 8, 14, 16axtgcgrrflx 25560 . . . . . . . 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 753 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
24 f1otrkg.2 . . . . . . . . . 10 ((𝜑 ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2524adantlr 753 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
264, 5, 6, 18, 19, 20, 21, 23, 25, 13, 15f1otrgds 25948 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
274, 5, 6, 18, 19, 20, 21, 23, 25, 15, 13f1otrgds 25948 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦𝐸𝑥) = ((𝐹𝑦)𝐷(𝐹𝑥)))
2817, 26, 273eqtr4d 2804 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
2928ralrimivva 3109 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
30 f1of1 6297 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵1-1𝑃)
319, 30syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵1-1𝑃)
32313ad2ant1 1128 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1𝑃)
33 simp21 1249 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥𝐵)
34 simp22 1250 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑦𝐵)
3533, 34jca 555 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐵𝑦𝐵))
3673ad2ant1 1128 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐺 ∈ TarskiG)
37113ad2ant1 1128 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵𝑃)
3837, 33ffvelrnd 6523 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) ∈ 𝑃)
3937, 34ffvelrnd 6523 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑦) ∈ 𝑃)
40 simp23 1251 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑧𝐵)
4137, 40ffvelrnd 6523 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑧) ∈ 𝑃)
42 simp3 1133 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = (𝑧𝐸𝑧))
4393ad2ant1 1128 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1-onto𝑃)
44223ad2antl1 1201 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
45243ad2antl1 1201 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
464, 5, 6, 18, 19, 20, 43, 44, 45, 33, 34f1otrgds 25948 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
474, 5, 6, 18, 19, 20, 43, 44, 45, 40, 40f1otrgds 25948 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑧𝐸𝑧) = ((𝐹𝑧)𝐷(𝐹𝑧)))
4842, 46, 473eqtr3d 2802 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑧)𝐷(𝐹𝑧)))
494, 5, 6, 36, 38, 39, 41, 48axtgcgrid 25561 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) = (𝐹𝑦))
50 f1veqaeq 6677 . . . . . . . . . 10 ((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
5150imp 444 . . . . . . . . 9 (((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
5232, 35, 49, 51syl21anc 1476 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 = 𝑦)
53523expia 1115 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5453ralrimivvva 3110 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5529, 54jca 555 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)))
5618, 19, 20istrkgc 25552 . . . . 5 (𝐻 ∈ TarskiGC ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))))
573, 55, 56sylanbrc 701 . . . 4 (𝜑𝐻 ∈ TarskiGC)
5893ad2ant1 1128 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1-onto𝑃)
5958, 30syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1𝑃)
60 simp2 1132 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑥𝐵𝑦𝐵))
6173ad2ant1 1128 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐺 ∈ TarskiG)
62143adant3 1127 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) ∈ 𝑃)
63163adant3 1127 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ 𝑃)
64 simp3 1133 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ (𝑥𝐽𝑥))
65223ad2antl1 1201 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
66243ad2antl1 1201 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
67133adant3 1127 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥𝐵)
68153adant3 1127 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦𝐵)
694, 5, 6, 18, 19, 20, 58, 65, 66, 67, 67, 68f1otrgitv 25949 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑦 ∈ (𝑥𝐽𝑥) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥))))
7064, 69mpbid 222 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥)))
714, 5, 6, 61, 62, 63, 70axtgbtwnid 25564 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) = (𝐹𝑦))
7259, 60, 71, 51syl21anc 1476 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 = 𝑦)
73723expia 1115 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
7473ralrimivva 3109 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
75 f1ocnv 6310 . . . . . . . . . . . . . 14 (𝐹:𝐵1-1-onto𝑃𝐹:𝑃1-1-onto𝐵)
76 f1of 6298 . . . . . . . . . . . . . 14 (𝐹:𝑃1-1-onto𝐵𝐹:𝑃𝐵)
779, 75, 763syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝑃𝐵)
7877ad5antr 775 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝑃𝐵)
79 simplr 809 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐𝑃)
8078, 79ffvelrnd 6523 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ 𝐵)
81 simpr 479 . . . . . . . . . . . . 13 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → 𝑎 = (𝐹𝑐))
8281eleq1d 2824 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑢𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑢𝐽𝑦)))
8381eleq1d 2824 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑣𝐽𝑥) ↔ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
8482, 83anbi12d 749 . . . . . . . . . . 11 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → ((𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)) ↔ ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥))))
85 simprl 811 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
8621ad2antrr 764 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵1-1-onto𝑃)
8786ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝐵1-1-onto𝑃)
88 f1ocnvfv2 6696 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → (𝐹‘(𝐹𝑐)) = 𝑐)
8988eleq1d 2824 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
9087, 79, 89syl2anc 696 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
9185, 90mpbird 247 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
92 simplll 815 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵)) → (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))))
93 simplll 815 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵)) → (𝜑 ∧ (𝑥𝐵𝑦𝐵)))
9493, 23sylancom 704 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
9592, 94sylancom 704 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
96 simplll 815 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))))
97 simplll 815 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝜑 ∧ (𝑥𝐵𝑦𝐵)))
9897, 25sylancom 704 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
9996, 98sylancom 704 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
100 simplr2 1263 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢𝐵)
101100ad2antrr 764 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑢𝐵)
10215ad2antrr 764 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑦𝐵)
103102ad2antrr 764 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑦𝐵)
1044, 5, 6, 18, 19, 20, 87, 95, 99, 101, 103, 80f1otrgitv 25949 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
10591, 104mpbird 247 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑢𝐽𝑦))
106 simprr 813 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
10788eleq1d 2824 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
10887, 79, 107syl2anc 696 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
109106, 108mpbird 247 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
110 simplr3 1265 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣𝐵)
111110ad2antrr 764 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑣𝐵)
11213ad2antrr 764 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑥𝐵)
113112ad2antrr 764 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑥𝐵)
1144, 5, 6, 18, 19, 20, 87, 95, 99, 111, 113, 80f1otrgitv 25949 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑣𝐽𝑥) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
115109, 114mpbird 247 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑣𝐽𝑥))
116105, 115jca 555 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
11780, 84, 116rspcedvd 3456 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
1188ad2antrr 764 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐺 ∈ TarskiG)
11912ad2antrr 764 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵𝑃)
120119, 112ffvelrnd 6523 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑥) ∈ 𝑃)
121119, 102ffvelrnd 6523 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑦) ∈ 𝑃)
122 simplr1 1261 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑧𝐵)
123119, 122ffvelrnd 6523 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑧) ∈ 𝑃)
124119, 100ffvelrnd 6523 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ 𝑃)
125119, 110ffvelrnd 6523 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ 𝑃)
126 simprl 811 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ (𝑥𝐽𝑧))
1274, 5, 6, 18, 19, 20, 86, 94, 98, 112, 122, 100f1otrgitv 25949 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑢 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
128126, 127mpbid 222 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
129 simprr 813 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ (𝑦𝐽𝑧))
1304, 5, 6, 18, 19, 20, 86, 94, 98, 102, 122, 110f1otrgitv 25949 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑣 ∈ (𝑦𝐽𝑧) ↔ (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧))))
131129, 130mpbid 222 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧)))
1324, 5, 6, 118, 120, 121, 123, 124, 125, 128, 131axtgpasch 25565 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑐𝑃 (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
133117, 132r19.29a 3216 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
134133ex 449 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
135134ralrimivvva 3110 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
136135ralrimivva 3109 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
1379ad5antr 775 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
138 simpllr 817 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
139137, 138, 88syl2anc 696 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) = 𝑐)
140 ffn 6206 . . . . . . . . . . . . . . . . . 18 (𝐹:𝐵𝑃𝐹 Fn 𝐵)
141137, 10, 1403syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹 Fn 𝐵)
142 simp-4r 827 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
143142simpld 477 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠 ∈ 𝒫 𝐵)
144143elpwid 4314 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
145144adantlr 753 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
146 simprl 811 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
147 fnfvima 6659 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝐵𝑠𝐵𝑥𝑠) → (𝐹𝑥) ∈ (𝐹𝑠))
148141, 145, 146, 147syl3anc 1477 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑥) ∈ (𝐹𝑠))
149142simprd 482 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡 ∈ 𝒫 𝐵)
150149elpwid 4314 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
151150adantlr 753 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
152 simprr 813 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
153 fnfvima 6659 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝐵𝑡𝐵𝑦𝑡) → (𝐹𝑦) ∈ (𝐹𝑡))
154141, 151, 152, 153syl3anc 1477 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑦) ∈ (𝐹𝑡))
155 simplr 809 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
156 oveq1 6820 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝐹𝑥) → (𝑒𝐼𝑓) = ((𝐹𝑥)𝐼𝑓))
157156eleq2d 2825 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝐹𝑥) → (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼𝑓)))
158 oveq2 6821 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝐹𝑦) → ((𝐹𝑥)𝐼𝑓) = ((𝐹𝑥)𝐼(𝐹𝑦)))
159158eleq2d 2825 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝐹𝑦) → (𝑐 ∈ ((𝐹𝑥)𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
160157, 159rspc2va 3462 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∈ (𝐹𝑠) ∧ (𝐹𝑦) ∈ (𝐹𝑡)) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
161148, 154, 155, 160syl21anc 1476 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
162139, 161eqeltrd 2839 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
1639ad4antr 771 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
164 simp-5l 829 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
165164, 22sylancom 704 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
166 simp-5l 829 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
167166, 24sylancom 704 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
168 simprl 811 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
169144, 168sseldd 3745 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝐵)
170 simprr 813 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
171150, 170sseldd 3745 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝐵)
17277ad4antr 771 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝑃𝐵)
173 simplr 809 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
174172, 173ffvelrnd 6523 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ 𝐵)
1754, 5, 6, 18, 19, 20, 163, 165, 167, 169, 171, 174f1otrgitv 25949 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
176175adantlr 753 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
177162, 176mpbird 247 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ (𝑥𝐽𝑦))
178177ralrimivva 3109 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
179178adantllr 757 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
18077ad4antr 771 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝐹:𝑃𝐵)
181 simpr 479 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝑐𝑃)
182180, 181ffvelrnd 6523 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (𝐹𝑐) ∈ 𝐵)
183 eleq1 2827 . . . . . . . . . . . . . . 15 (𝑏 = (𝐹𝑐) → (𝑏 ∈ (𝑥𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
1841832ralbidv 3127 . . . . . . . . . . . . . 14 (𝑏 = (𝐹𝑐) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
185184adantl 473 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ 𝑏 = (𝐹𝑐)) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
186182, 185rspcedv 3453 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
187186adantr 472 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
188179, 187mpd 15 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
1897ad3antrrr 768 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐺 ∈ TarskiG)
190 imassrn 5635 . . . . . . . . . . . 12 (𝐹𝑠) ⊆ ran 𝐹
191 f1ofo 6305 . . . . . . . . . . . . . 14 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵onto𝑃)
192 forn 6279 . . . . . . . . . . . . . 14 (𝐹:𝐵onto𝑃 → ran 𝐹 = 𝑃)
1939, 191, 1923syl 18 . . . . . . . . . . . . 13 (𝜑 → ran 𝐹 = 𝑃)
194193ad3antrrr 768 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ran 𝐹 = 𝑃)
195190, 194syl5sseq 3794 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑠) ⊆ 𝑃)
196 imassrn 5635 . . . . . . . . . . . 12 (𝐹𝑡) ⊆ ran 𝐹
197196, 194syl5sseq 3794 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑡) ⊆ 𝑃)
19811ad3antrrr 768 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐹:𝐵𝑃)
199 simplr 809 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝑎𝐵)
200198, 199ffvelrnd 6523 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑎) ∈ 𝑃)
2019ad5antr 775 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1-onto𝑃)
202 ffn 6206 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑃𝐵𝐹 Fn 𝑃)
203201, 75, 76, 2024syl 19 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹 Fn 𝑃)
204195ad2antrr 764 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑠) ⊆ 𝑃)
205 simplr 809 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ (𝐹𝑠))
206 fnfvima 6659 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑃 ∧ (𝐹𝑠) ⊆ 𝑃𝑢 ∈ (𝐹𝑠)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
207203, 204, 205, 206syl3anc 1477 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
208201, 30syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1𝑃)
209 simp-5r 831 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
210209simpld 477 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠 ∈ 𝒫 𝐵)
211210elpwid 4314 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠𝐵)
212 f1imacnv 6314 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐵1-1𝑃𝑠𝐵) → (𝐹 “ (𝐹𝑠)) = 𝑠)
213208, 211, 212syl2anc 696 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑠)) = 𝑠)
214207, 213eleqtrd 2841 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝑠)
215197ad2antrr 764 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑡) ⊆ 𝑃)
216 simpr 479 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣 ∈ (𝐹𝑡))
217 fnfvima 6659 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑃 ∧ (𝐹𝑡) ⊆ 𝑃𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
218203, 215, 216, 217syl3anc 1477 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
219209simprd 482 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡 ∈ 𝒫 𝐵)
220219elpwid 4314 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡𝐵)
221 f1imacnv 6314 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐵1-1𝑃𝑡𝐵) → (𝐹 “ (𝐹𝑡)) = 𝑡)
222208, 220, 221syl2anc 696 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑡)) = 𝑡)
223218, 222eleqtrd 2841 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝑡)
224 simpllr 817 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦))
225 eleq1 2827 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐹𝑢) → (𝑥 ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽𝑦)))
226 oveq2 6821 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐹𝑣) → (𝑎𝐽𝑦) = (𝑎𝐽(𝐹𝑣)))
227226eleq2d 2825 . . . . . . . . . . . . . . . 16 (𝑦 = (𝐹𝑣) → ((𝐹𝑢) ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣))))
228225, 227rspc2va 3462 . . . . . . . . . . . . . . 15 ((((𝐹𝑢) ∈ 𝑠 ∧ (𝐹𝑣) ∈ 𝑡) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
229214, 223, 224, 228syl21anc 1476 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
230 simp-6l 833 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
231230, 22sylancom 704 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
232 simp-6l 833 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
233232, 24sylancom 704 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
234 simp-4r 827 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑎𝐵)
235215, 216sseldd 3745 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣𝑃)
236 f1ocnvdm 6703 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹𝑣) ∈ 𝐵)
237201, 235, 236syl2anc 696 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝐵)
238204, 205sseldd 3745 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢𝑃)
239 f1ocnvdm 6703 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹𝑢) ∈ 𝐵)
240201, 238, 239syl2anc 696 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝐵)
2414, 5, 6, 18, 19, 20, 201, 231, 233, 234, 237, 240f1otrgitv 25949 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)) ↔ (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣)))))
242229, 241mpbid 222 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))))
243 f1ocnvfv2 6696 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹‘(𝐹𝑢)) = 𝑢)
244201, 238, 243syl2anc 696 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) = 𝑢)
245 f1ocnvfv2 6696 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹‘(𝐹𝑣)) = 𝑣)
246201, 235, 245syl2anc 696 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑣)) = 𝑣)
247246oveq2d 6829 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))) = ((𝐹𝑎)𝐼𝑣))
248242, 244, 2473eltr3d 2853 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2492483impa 1101 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2504, 5, 6, 189, 195, 197, 200, 249axtgcont 25567 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑐𝑃𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
251188, 250r19.29a 3216 . . . . . . . . 9 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
252251r19.29an 3215 . . . . . . . 8 (((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ ∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
253252ex 449 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
254253ralrimivva 3109 . . . . . 6 (𝜑 → ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
25574, 136, 2543jca 1123 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))))
25618, 19, 20istrkgb 25553 . . . . 5 (𝐻 ∈ TarskiGB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))))
2573, 255, 256sylanbrc 701 . . . 4 (𝜑𝐻 ∈ TarskiGB)
25857, 257elind 3941 . . 3 (𝜑𝐻 ∈ (TarskiGC ∩ TarskiGB))
2597ad9antr 791 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐺 ∈ TarskiG)
26011ad9antr 791 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵𝑃)
261 simp-9r 847 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝐵)
262260, 261ffvelrnd 6523 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ∈ 𝑃)
263 simp-8r 843 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦𝐵)
264260, 263ffvelrnd 6523 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ 𝑃)
265 simp-7r 839 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑧𝐵)
266260, 265ffvelrnd 6523 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑧) ∈ 𝑃)
267 simp-5r 831 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑎𝐵)
268260, 267ffvelrnd 6523 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑎) ∈ 𝑃)
269 simp-4r 827 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏𝐵)
270260, 269ffvelrnd 6523 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ 𝑃)
271 simpllr 817 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑐𝐵)
272260, 271ffvelrnd 6523 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑐) ∈ 𝑃)
273 simp-6r 835 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑢𝐵)
274260, 273ffvelrnd 6523 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑢) ∈ 𝑃)
275 simplr 809 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑣𝐵)
276260, 275ffvelrnd 6523 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑣) ∈ 𝑃)
2779ad9antr 791 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵1-1-onto𝑃)
278277, 261jca 555 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹:𝐵1-1-onto𝑃𝑥𝐵))
279 simprl1 1267 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝑦)
280 dff1o6 6694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
281280simp3bi 1142 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝐵1-1-onto𝑃 → ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
282281r19.21bi 3070 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐵1-1-onto𝑃𝑥𝐵) → ∀𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
283282r19.21bi 3070 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
284283necon3d 2953 . . . . . . . . . . . . . . . . . . 19 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → (𝑥𝑦 → (𝐹𝑥) ≠ (𝐹𝑦)))
285284imp 444 . . . . . . . . . . . . . . . . . 18 ((((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝑦) → (𝐹𝑥) ≠ (𝐹𝑦))
286278, 263, 279, 285syl21anc 1476 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ≠ (𝐹𝑦))
287 simprl2 1269 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ (𝑥𝐽𝑧))
28822ex 449 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
289288ad9antr 791 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
290289imp 444 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
29124ex 449 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
292291ad9antr 791 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
293292imp 444 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2944, 5, 6, 18, 19, 20, 277, 290, 293, 261, 265, 263f1otrgitv 25949 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
295287, 294mpbid 222 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
296 simprl3 1271 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ (𝑎𝐽𝑐))
2974, 5, 6, 18, 19, 20, 277, 290, 293, 267, 271, 269f1otrgitv 25949 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏 ∈ (𝑎𝐽𝑐) ↔ (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐))))
298296, 297mpbid 222 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐)))
299 simprr 813 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))
300299simpld 477 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)))
301300simpld 477 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = (𝑎𝐸𝑏))
3024, 5, 6, 18, 19, 20, 277, 290, 293, 261, 263f1otrgds 25948 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
3034, 5, 6, 18, 19, 20, 277, 290, 293, 267, 269f1otrgds 25948 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
304301, 302, 3033eqtr3d 2802 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
305300simprd 482 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = (𝑏𝐸𝑐))
3064, 5, 6, 18, 19, 20, 277, 290, 293, 263, 265f1otrgds 25948 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = ((𝐹𝑦)𝐷(𝐹𝑧)))
3074, 5, 6, 18, 19, 20, 277, 290, 293, 269, 271f1otrgds 25948 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑐) = ((𝐹𝑏)𝐷(𝐹𝑐)))
308305, 306, 3073eqtr3d 2802 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑧)) = ((𝐹𝑏)𝐷(𝐹𝑐)))
309299simprd 482 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))
310309simpld 477 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = (𝑎𝐸𝑣))
3114, 5, 6, 18, 19, 20, 277, 290, 293, 261, 273f1otrgds 25948 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = ((𝐹𝑥)𝐷(𝐹𝑢)))
3124, 5, 6, 18, 19, 20, 277, 290, 293, 267, 275f1otrgds 25948 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑣) = ((𝐹𝑎)𝐷(𝐹𝑣)))
313310, 311, 3123eqtr3d 2802 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑢)) = ((𝐹𝑎)𝐷(𝐹𝑣)))
314309simprd 482 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = (𝑏𝐸𝑣))
3154, 5, 6, 18, 19, 20, 277, 290, 293, 263, 273f1otrgds 25948 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = ((𝐹𝑦)𝐷(𝐹𝑢)))
3164, 5, 6, 18, 19, 20, 277, 290, 293, 269, 275f1otrgds 25948 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑣) = ((𝐹𝑏)𝐷(𝐹𝑣)))
317314, 315, 3163eqtr3d 2802 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑢)) = ((𝐹𝑏)𝐷(𝐹𝑣)))
3184, 5, 6, 259, 262, 264, 266, 268, 270, 272, 274, 276, 286, 295, 298, 304, 308, 313, 317axtg5seg 25563 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑧)𝐷(𝐹𝑢)) = ((𝐹𝑐)𝐷(𝐹𝑣)))
3194, 5, 6, 18, 19, 20, 277, 290, 293, 265, 273f1otrgds 25948 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = ((𝐹𝑧)𝐷(𝐹𝑢)))
3204, 5, 6, 18, 19, 20, 277, 290, 293, 271, 275f1otrgds 25948 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑐𝐸𝑣) = ((𝐹𝑐)𝐷(𝐹𝑣)))
321318, 319, 3203eqtr4d 2804 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))
322321ex 449 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) → (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
323322ralrimiva 3104 . . . . . . . . . . . . 13 ((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) → ∀𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
324323ralrimiva 3104 . . . . . . . . . . . 12 (((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) → ∀𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
325324ralrimiva 3104 . . . . . . . . . . 11 ((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) → ∀𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
326325ralrimiva 3104 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) → ∀𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
327326ralrimiva 3104 . . . . . . . . 9 ((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) → ∀𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
328327ralrimiva 3104 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → ∀𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
329328ralrimiva 3104 . . . . . . 7 ((𝜑𝑥𝐵) → ∀𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
330329ralrimiva 3104 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
331 simp-4l 825 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝜑)
332 simplr 809 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑤𝑃)
333 simprl 811 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤))
334331, 9syl 17 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝐹:𝐵1-1-onto𝑃)
335 f1ocnvfv2 6696 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑤𝑃) → (𝐹‘(𝐹𝑤)) = 𝑤)
336334, 332, 335syl2anc 696 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹‘(𝐹𝑤)) = 𝑤)
337336oveq2d 6829 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))) = ((𝐹𝑥)𝐼𝑤))
338333, 337eleqtrrd 2842 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))))
339331, 22sylan 489 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
340331, 24sylan 489 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
34113ad3antrrr 768 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑥𝐵)
34277ffvelrnda 6522 . . . . . . . . . . . . 13 ((𝜑𝑤𝑃) → (𝐹𝑤) ∈ 𝐵)
343331, 332, 342syl2anc 696 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑤) ∈ 𝐵)
34415ad3antrrr 768 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦𝐵)
3454, 5, 6, 18, 19, 20, 334, 339, 340, 341, 343, 344f1otrgitv 25949 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤)))))
346338, 345mpbird 247 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦 ∈ (𝑥𝐽(𝐹𝑤)))
3474, 5, 6, 18, 19, 20, 334, 339, 340, 344, 343f1otrgds 25948 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))))
348336oveq2d 6829 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))) = ((𝐹𝑦)𝐷𝑤))
349 simprr 813 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))
350347, 348, 3493eqtrd 2798 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
351 simprl 811 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑎𝐵)
352351ad2antrr 764 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑎𝐵)
353 simprr 813 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑏𝐵)
354353ad2antrr 764 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑏𝐵)
3554, 5, 6, 18, 19, 20, 334, 339, 340, 352, 354f1otrgds 25948 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
356350, 355eqtr4d 2797 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))
357 oveq2 6821 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑥𝐽𝑧) = (𝑥𝐽(𝐹𝑤)))
358357eleq2d 2825 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ 𝑦 ∈ (𝑥𝐽(𝐹𝑤))))
359 oveq2 6821 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑦𝐸𝑧) = (𝑦𝐸(𝐹𝑤)))
360359eqeq1d 2762 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → ((𝑦𝐸𝑧) = (𝑎𝐸𝑏) ↔ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)))
361358, 360anbi12d 749 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑤) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
362361adantl 473 . . . . . . . . . . . 12 (((𝜑𝑤𝑃) ∧ 𝑧 = (𝐹𝑤)) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
363342, 362rspcedv 3453 . . . . . . . . . . 11 ((𝜑𝑤𝑃) → ((𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))
364363imp 444 . . . . . . . . . 10 (((𝜑𝑤𝑃) ∧ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
365331, 332, 346, 356, 364syl22anc 1478 . . . . . . . . 9 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3668adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐺 ∈ TarskiG)
36714adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑥) ∈ 𝑃)
36816adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑦) ∈ 𝑃)
36912adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐹:𝐵𝑃)
370369, 351ffvelrnd 6523 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑎) ∈ 𝑃)
371369, 353ffvelrnd 6523 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑏) ∈ 𝑃)
3724, 5, 6, 366, 367, 368, 370, 371axtgsegcon 25562 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑤𝑃 ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏))))
373365, 372r19.29a 3216 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
374373ralrimivva 3109 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
375374ralrimivva 3109 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3763, 330, 375jca32 559 . . . . 5 (𝜑 → (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
37718, 19, 20istrkgcb 25554 . . . . 5 (𝐻 ∈ TarskiGCB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
378376, 377sylibr 224 . . . 4 (𝜑𝐻 ∈ TarskiGCB)
379 f1otrg.l . . . . 5 (𝜑 → (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))
38018, 19, 20istrkgl 25556 . . . . 5 (𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))})))
3813, 379, 380sylanbrc 701 . . . 4 (𝜑𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
382378, 381elind 3941 . . 3 (𝜑𝐻 ∈ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
383258, 382elind 3941 . 2 (𝜑𝐻 ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})))
384 df-trkg 25551 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
385383, 384syl6eleqr 2850 1 (𝜑𝐻 ∈ TarskiG)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3o 1071  w3a 1072   = wceq 1632  wcel 2139  {cab 2746  wne 2932  wral 3050  wrex 3051  {crab 3054  Vcvv 3340  [wsbc 3576  cdif 3712  cin 3714  wss 3715  𝒫 cpw 4302  {csn 4321  ccnv 5265  ran crn 5267  cima 5269   Fn wfn 6044  wf 6045  1-1wf1 6046  ontowfo 6047  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6813  cmpt2 6815  Basecbs 16059  distcds 16152  TarskiGcstrkg 25528  TarskiGCcstrkgc 25529  TarskiGBcstrkgb 25530  TarskiGCBcstrkgcb 25531  Itvcitv 25534  LineGclng 25535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-trkgc 25546  df-trkgb 25547  df-trkgcb 25548  df-trkg 25551
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator