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

Theorem f1otrg 25551
 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 3185 . . . . . 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 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐺 ∈ TarskiG)
9 f1otrkg.f . . . . . . . . . . . 12 (𝜑𝐹:𝐵1-1-onto𝑃)
10 f1of 6050 . . . . . . . . . . . 12 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵𝑃)
119, 10syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝑃)
1211adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹:𝐵𝑃)
13 simprl 790 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
1412, 13ffvelrnd 6268 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑥) ∈ 𝑃)
15 simprr 792 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
1612, 15ffvelrnd 6268 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑦) ∈ 𝑃)
174, 5, 6, 8, 14, 16axtgcgrrflx 25161 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑦)𝐷(𝐹𝑥)))
18 f1otrkg.b . . . . . . . . 9 𝐵 = (Base‘𝐻)
19 f1otrkg.e . . . . . . . . 9 𝐸 = (dist‘𝐻)
20 f1otrkg.j . . . . . . . . 9 𝐽 = (Itv‘𝐻)
219adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹:𝐵1-1-onto𝑃)
22 f1otrkg.1 . . . . . . . . . 10 ((𝜑 ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
2322adantlr 747 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
24 f1otrkg.2 . . . . . . . . . 10 ((𝜑 ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2524adantlr 747 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
264, 5, 6, 18, 19, 20, 21, 23, 25, 13, 15f1otrgds 25549 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
274, 5, 6, 18, 19, 20, 21, 23, 25, 15, 13f1otrgds 25549 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦𝐸𝑥) = ((𝐹𝑦)𝐷(𝐹𝑥)))
2817, 26, 273eqtr4d 2654 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
2928ralrimivva 2954 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
30 f1of1 6049 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵1-1𝑃)
319, 30syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵1-1𝑃)
32313ad2ant1 1075 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1𝑃)
33 simp21 1087 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥𝐵)
34 simp22 1088 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑦𝐵)
3533, 34jca 553 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐵𝑦𝐵))
3673ad2ant1 1075 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐺 ∈ TarskiG)
37113ad2ant1 1075 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵𝑃)
3837, 33ffvelrnd 6268 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) ∈ 𝑃)
3937, 34ffvelrnd 6268 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑦) ∈ 𝑃)
40 simp23 1089 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑧𝐵)
4137, 40ffvelrnd 6268 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑧) ∈ 𝑃)
42 simp3 1056 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = (𝑧𝐸𝑧))
4393ad2ant1 1075 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1-onto𝑃)
44223ad2antl1 1216 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
45243ad2antl1 1216 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
464, 5, 6, 18, 19, 20, 43, 44, 45, 33, 34f1otrgds 25549 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
474, 5, 6, 18, 19, 20, 43, 44, 45, 40, 40f1otrgds 25549 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑧𝐸𝑧) = ((𝐹𝑧)𝐷(𝐹𝑧)))
4842, 46, 473eqtr3d 2652 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑧)𝐷(𝐹𝑧)))
494, 5, 6, 36, 38, 39, 41, 48axtgcgrid 25162 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) = (𝐹𝑦))
50 f1veqaeq 6418 . . . . . . . . . 10 ((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
5150imp 444 . . . . . . . . 9 (((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
5232, 35, 49, 51syl21anc 1317 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 = 𝑦)
53523expia 1259 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5453ralrimivvva 2955 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5529, 54jca 553 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)))
5618, 19, 20istrkgc 25153 . . . . 5 (𝐻 ∈ TarskiGC ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))))
573, 55, 56sylanbrc 695 . . . 4 (𝜑𝐻 ∈ TarskiGC)
5893ad2ant1 1075 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1-onto𝑃)
5958, 30syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1𝑃)
60 simp2 1055 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑥𝐵𝑦𝐵))
6173ad2ant1 1075 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐺 ∈ TarskiG)
62143adant3 1074 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) ∈ 𝑃)
63163adant3 1074 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ 𝑃)
64 simp3 1056 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ (𝑥𝐽𝑥))
65223ad2antl1 1216 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
66243ad2antl1 1216 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
67133adant3 1074 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥𝐵)
68153adant3 1074 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦𝐵)
694, 5, 6, 18, 19, 20, 58, 65, 66, 67, 67, 68f1otrgitv 25550 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑦 ∈ (𝑥𝐽𝑥) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥))))
7064, 69mpbid 221 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥)))
714, 5, 6, 61, 62, 63, 70axtgbtwnid 25165 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) = (𝐹𝑦))
7259, 60, 71, 51syl21anc 1317 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 = 𝑦)
73723expia 1259 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
7473ralrimivva 2954 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
75 f1ocnv 6062 . . . . . . . . . . . . . 14 (𝐹:𝐵1-1-onto𝑃𝐹:𝑃1-1-onto𝐵)
76 f1of 6050 . . . . . . . . . . . . . 14 (𝐹:𝑃1-1-onto𝐵𝐹:𝑃𝐵)
779, 75, 763syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝑃𝐵)
7877ad5antr 766 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝑃𝐵)
79 simplr 788 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐𝑃)
8078, 79ffvelrnd 6268 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ 𝐵)
81 simpr 476 . . . . . . . . . . . . 13 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → 𝑎 = (𝐹𝑐))
8281eleq1d 2672 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑢𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑢𝐽𝑦)))
8381eleq1d 2672 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑣𝐽𝑥) ↔ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
8482, 83anbi12d 743 . . . . . . . . . . 11 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → ((𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)) ↔ ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥))))
85 simprl 790 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
8621ad2antrr 758 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵1-1-onto𝑃)
8786ad2antrr 758 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝐵1-1-onto𝑃)
88 f1ocnvfv2 6433 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → (𝐹‘(𝐹𝑐)) = 𝑐)
8988eleq1d 2672 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
9087, 79, 89syl2anc 691 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
9185, 90mpbird 246 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
92 simplll 794 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵)) → (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))))
93 simplll 794 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵)) → (𝜑 ∧ (𝑥𝐵𝑦𝐵)))
9493, 23sylancom 698 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
9592, 94sylancom 698 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
96 simplll 794 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))))
97 simplll 794 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝜑 ∧ (𝑥𝐵𝑦𝐵)))
9897, 25sylancom 698 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
9996, 98sylancom 698 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
100 simplr2 1097 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢𝐵)
101100ad2antrr 758 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑢𝐵)
10215ad2antrr 758 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑦𝐵)
103102ad2antrr 758 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑦𝐵)
1044, 5, 6, 18, 19, 20, 87, 95, 99, 101, 103, 80f1otrgitv 25550 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
10591, 104mpbird 246 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑢𝐽𝑦))
106 simprr 792 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
10788eleq1d 2672 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
10887, 79, 107syl2anc 691 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
109106, 108mpbird 246 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
110 simplr3 1098 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣𝐵)
111110ad2antrr 758 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑣𝐵)
11213ad2antrr 758 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑥𝐵)
113112ad2antrr 758 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑥𝐵)
1144, 5, 6, 18, 19, 20, 87, 95, 99, 111, 113, 80f1otrgitv 25550 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑣𝐽𝑥) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
115109, 114mpbird 246 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑣𝐽𝑥))
116105, 115jca 553 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
11780, 84, 116rspcedvd 3289 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
1188ad2antrr 758 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐺 ∈ TarskiG)
11912ad2antrr 758 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵𝑃)
120119, 112ffvelrnd 6268 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑥) ∈ 𝑃)
121119, 102ffvelrnd 6268 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑦) ∈ 𝑃)
122 simplr1 1096 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑧𝐵)
123119, 122ffvelrnd 6268 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑧) ∈ 𝑃)
124119, 100ffvelrnd 6268 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ 𝑃)
125119, 110ffvelrnd 6268 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ 𝑃)
126 simprl 790 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ (𝑥𝐽𝑧))
1274, 5, 6, 18, 19, 20, 86, 94, 98, 112, 122, 100f1otrgitv 25550 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑢 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
128126, 127mpbid 221 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
129 simprr 792 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ (𝑦𝐽𝑧))
1304, 5, 6, 18, 19, 20, 86, 94, 98, 102, 122, 110f1otrgitv 25550 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑣 ∈ (𝑦𝐽𝑧) ↔ (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧))))
131129, 130mpbid 221 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧)))
1324, 5, 6, 118, 120, 121, 123, 124, 125, 128, 131axtgpasch 25166 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑐𝑃 (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
133117, 132r19.29a 3060 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
134133ex 449 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
135134ralrimivvva 2955 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
136135ralrimivva 2954 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
1379ad5antr 766 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
138 simpllr 795 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
139137, 138, 88syl2anc 691 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) = 𝑐)
140 ffn 5958 . . . . . . . . . . . . . . . . . 18 (𝐹:𝐵𝑃𝐹 Fn 𝐵)
141137, 10, 1403syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹 Fn 𝐵)
142 simp-4r 803 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
143142simpld 474 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠 ∈ 𝒫 𝐵)
144143elpwid 4118 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
145144adantlr 747 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
146 simprl 790 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
147 fnfvima 6400 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝐵𝑠𝐵𝑥𝑠) → (𝐹𝑥) ∈ (𝐹𝑠))
148141, 145, 146, 147syl3anc 1318 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑥) ∈ (𝐹𝑠))
149142simprd 478 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡 ∈ 𝒫 𝐵)
150149elpwid 4118 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
151150adantlr 747 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
152 simprr 792 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
153 fnfvima 6400 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝐵𝑡𝐵𝑦𝑡) → (𝐹𝑦) ∈ (𝐹𝑡))
154141, 151, 152, 153syl3anc 1318 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑦) ∈ (𝐹𝑡))
155 simplr 788 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
156 oveq1 6556 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝐹𝑥) → (𝑒𝐼𝑓) = ((𝐹𝑥)𝐼𝑓))
157156eleq2d 2673 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝐹𝑥) → (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼𝑓)))
158 oveq2 6557 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝐹𝑦) → ((𝐹𝑥)𝐼𝑓) = ((𝐹𝑥)𝐼(𝐹𝑦)))
159158eleq2d 2673 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝐹𝑦) → (𝑐 ∈ ((𝐹𝑥)𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
160157, 159rspc2va 3294 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∈ (𝐹𝑠) ∧ (𝐹𝑦) ∈ (𝐹𝑡)) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
161148, 154, 155, 160syl21anc 1317 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
162139, 161eqeltrd 2688 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
1639ad4antr 764 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
164 simp-5l 804 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
165164, 22sylancom 698 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
166 simp-5l 804 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
167166, 24sylancom 698 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
168 simprl 790 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
169144, 168sseldd 3569 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝐵)
170 simprr 792 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
171150, 170sseldd 3569 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝐵)
17277ad4antr 764 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝑃𝐵)
173 simplr 788 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
174172, 173ffvelrnd 6268 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ 𝐵)
1754, 5, 6, 18, 19, 20, 163, 165, 167, 169, 171, 174f1otrgitv 25550 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
176175adantlr 747 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
177162, 176mpbird 246 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ (𝑥𝐽𝑦))
178177ralrimivva 2954 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
179178adantllr 751 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
18077ad4antr 764 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝐹:𝑃𝐵)
181 simpr 476 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝑐𝑃)
182180, 181ffvelrnd 6268 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (𝐹𝑐) ∈ 𝐵)
183 eleq1 2676 . . . . . . . . . . . . . . 15 (𝑏 = (𝐹𝑐) → (𝑏 ∈ (𝑥𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
1841832ralbidv 2972 . . . . . . . . . . . . . 14 (𝑏 = (𝐹𝑐) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
185184adantl 481 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ 𝑏 = (𝐹𝑐)) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
186182, 185rspcedv 3286 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
187186adantr 480 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
188179, 187mpd 15 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
1897ad3antrrr 762 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐺 ∈ TarskiG)
190 imassrn 5396 . . . . . . . . . . . 12 (𝐹𝑠) ⊆ ran 𝐹
191 f1ofo 6057 . . . . . . . . . . . . . 14 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵onto𝑃)
192 forn 6031 . . . . . . . . . . . . . 14 (𝐹:𝐵onto𝑃 → ran 𝐹 = 𝑃)
1939, 191, 1923syl 18 . . . . . . . . . . . . 13 (𝜑 → ran 𝐹 = 𝑃)
194193ad3antrrr 762 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ran 𝐹 = 𝑃)
195190, 194syl5sseq 3616 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑠) ⊆ 𝑃)
196 imassrn 5396 . . . . . . . . . . . 12 (𝐹𝑡) ⊆ ran 𝐹
197196, 194syl5sseq 3616 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑡) ⊆ 𝑃)
19811ad3antrrr 762 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐹:𝐵𝑃)
199 simplr 788 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝑎𝐵)
200198, 199ffvelrnd 6268 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑎) ∈ 𝑃)
2019ad5antr 766 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1-onto𝑃)
202 ffn 5958 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑃𝐵𝐹 Fn 𝑃)
203201, 75, 76, 2024syl 19 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹 Fn 𝑃)
204195ad2antrr 758 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑠) ⊆ 𝑃)
205 simplr 788 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ (𝐹𝑠))
206 fnfvima 6400 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑃 ∧ (𝐹𝑠) ⊆ 𝑃𝑢 ∈ (𝐹𝑠)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
207203, 204, 205, 206syl3anc 1318 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
208201, 30syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1𝑃)
209 simp-5r 805 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
210209simpld 474 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠 ∈ 𝒫 𝐵)
211210elpwid 4118 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠𝐵)
212 f1imacnv 6066 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐵1-1𝑃𝑠𝐵) → (𝐹 “ (𝐹𝑠)) = 𝑠)
213208, 211, 212syl2anc 691 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑠)) = 𝑠)
214207, 213eleqtrd 2690 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝑠)
215197ad2antrr 758 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑡) ⊆ 𝑃)
216 simpr 476 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣 ∈ (𝐹𝑡))
217 fnfvima 6400 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑃 ∧ (𝐹𝑡) ⊆ 𝑃𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
218203, 215, 216, 217syl3anc 1318 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
219209simprd 478 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡 ∈ 𝒫 𝐵)
220219elpwid 4118 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡𝐵)
221 f1imacnv 6066 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐵1-1𝑃𝑡𝐵) → (𝐹 “ (𝐹𝑡)) = 𝑡)
222208, 220, 221syl2anc 691 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑡)) = 𝑡)
223218, 222eleqtrd 2690 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝑡)
224 simpllr 795 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦))
225 eleq1 2676 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐹𝑢) → (𝑥 ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽𝑦)))
226 oveq2 6557 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐹𝑣) → (𝑎𝐽𝑦) = (𝑎𝐽(𝐹𝑣)))
227226eleq2d 2673 . . . . . . . . . . . . . . . 16 (𝑦 = (𝐹𝑣) → ((𝐹𝑢) ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣))))
228225, 227rspc2va 3294 . . . . . . . . . . . . . . 15 ((((𝐹𝑢) ∈ 𝑠 ∧ (𝐹𝑣) ∈ 𝑡) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
229214, 223, 224, 228syl21anc 1317 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
230 simp-6l 806 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
231230, 22sylancom 698 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
232 simp-6l 806 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
233232, 24sylancom 698 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
234 simp-4r 803 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑎𝐵)
235215, 216sseldd 3569 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣𝑃)
236 f1ocnvdm 6440 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹𝑣) ∈ 𝐵)
237201, 235, 236syl2anc 691 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝐵)
238204, 205sseldd 3569 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢𝑃)
239 f1ocnvdm 6440 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹𝑢) ∈ 𝐵)
240201, 238, 239syl2anc 691 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝐵)
2414, 5, 6, 18, 19, 20, 201, 231, 233, 234, 237, 240f1otrgitv 25550 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)) ↔ (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣)))))
242229, 241mpbid 221 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))))
243 f1ocnvfv2 6433 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹‘(𝐹𝑢)) = 𝑢)
244201, 238, 243syl2anc 691 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) = 𝑢)
245 f1ocnvfv2 6433 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹‘(𝐹𝑣)) = 𝑣)
246201, 235, 245syl2anc 691 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑣)) = 𝑣)
247246oveq2d 6565 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))) = ((𝐹𝑎)𝐼𝑣))
248242, 244, 2473eltr3d 2702 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2492483impa 1251 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2504, 5, 6, 189, 195, 197, 200, 249axtgcont 25168 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑐𝑃𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
251188, 250r19.29a 3060 . . . . . . . . 9 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
252251r19.29an 3059 . . . . . . . 8 (((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ ∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
253252ex 449 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
254253ralrimivva 2954 . . . . . 6 (𝜑 → ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
25574, 136, 2543jca 1235 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))))
25618, 19, 20istrkgb 25154 . . . . 5 (𝐻 ∈ TarskiGB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))))
2573, 255, 256sylanbrc 695 . . . 4 (𝜑𝐻 ∈ TarskiGB)
25857, 257elind 3760 . . 3 (𝜑𝐻 ∈ (TarskiGC ∩ TarskiGB))
2597ad9antr 774 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐺 ∈ TarskiG)
26011ad9antr 774 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵𝑃)
261 simp-9r 813 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝐵)
262260, 261ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ∈ 𝑃)
263 simp-8r 811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦𝐵)
264260, 263ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ 𝑃)
265 simp-7r 809 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑧𝐵)
266260, 265ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑧) ∈ 𝑃)
267 simp-5r 805 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑎𝐵)
268260, 267ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑎) ∈ 𝑃)
269 simp-4r 803 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏𝐵)
270260, 269ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ 𝑃)
271 simpllr 795 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑐𝐵)
272260, 271ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑐) ∈ 𝑃)
273 simp-6r 807 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑢𝐵)
274260, 273ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑢) ∈ 𝑃)
275 simplr 788 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑣𝐵)
276260, 275ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑣) ∈ 𝑃)
2779ad9antr 774 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵1-1-onto𝑃)
278277, 261jca 553 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹:𝐵1-1-onto𝑃𝑥𝐵))
279 simprl1 1099 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝑦)
280 dff1o6 6431 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
281280simp3bi 1071 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝐵1-1-onto𝑃 → ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
282281r19.21bi 2916 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐵1-1-onto𝑃𝑥𝐵) → ∀𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
283282r19.21bi 2916 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
284283necon3d 2803 . . . . . . . . . . . . . . . . . . 19 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → (𝑥𝑦 → (𝐹𝑥) ≠ (𝐹𝑦)))
285284imp 444 . . . . . . . . . . . . . . . . . 18 ((((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝑦) → (𝐹𝑥) ≠ (𝐹𝑦))
286278, 263, 279, 285syl21anc 1317 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ≠ (𝐹𝑦))
287 simprl2 1100 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ (𝑥𝐽𝑧))
28822ex 449 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
289288ad9antr 774 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
290289imp 444 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
29124ex 449 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
292291ad9antr 774 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
293292imp 444 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2944, 5, 6, 18, 19, 20, 277, 290, 293, 261, 265, 263f1otrgitv 25550 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
295287, 294mpbid 221 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
296 simprl3 1101 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ (𝑎𝐽𝑐))
2974, 5, 6, 18, 19, 20, 277, 290, 293, 267, 271, 269f1otrgitv 25550 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏 ∈ (𝑎𝐽𝑐) ↔ (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐))))
298296, 297mpbid 221 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐)))
299 simprr 792 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))
300299simpld 474 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)))
301300simpld 474 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = (𝑎𝐸𝑏))
3024, 5, 6, 18, 19, 20, 277, 290, 293, 261, 263f1otrgds 25549 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
3034, 5, 6, 18, 19, 20, 277, 290, 293, 267, 269f1otrgds 25549 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
304301, 302, 3033eqtr3d 2652 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
305300simprd 478 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = (𝑏𝐸𝑐))
3064, 5, 6, 18, 19, 20, 277, 290, 293, 263, 265f1otrgds 25549 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = ((𝐹𝑦)𝐷(𝐹𝑧)))
3074, 5, 6, 18, 19, 20, 277, 290, 293, 269, 271f1otrgds 25549 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑐) = ((𝐹𝑏)𝐷(𝐹𝑐)))
308305, 306, 3073eqtr3d 2652 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑧)) = ((𝐹𝑏)𝐷(𝐹𝑐)))
309299simprd 478 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))
310309simpld 474 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = (𝑎𝐸𝑣))
3114, 5, 6, 18, 19, 20, 277, 290, 293, 261, 273f1otrgds 25549 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = ((𝐹𝑥)𝐷(𝐹𝑢)))
3124, 5, 6, 18, 19, 20, 277, 290, 293, 267, 275f1otrgds 25549 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑣) = ((𝐹𝑎)𝐷(𝐹𝑣)))
313310, 311, 3123eqtr3d 2652 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑢)) = ((𝐹𝑎)𝐷(𝐹𝑣)))
314309simprd 478 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = (𝑏𝐸𝑣))
3154, 5, 6, 18, 19, 20, 277, 290, 293, 263, 273f1otrgds 25549 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = ((𝐹𝑦)𝐷(𝐹𝑢)))
3164, 5, 6, 18, 19, 20, 277, 290, 293, 269, 275f1otrgds 25549 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑣) = ((𝐹𝑏)𝐷(𝐹𝑣)))
317314, 315, 3163eqtr3d 2652 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑢)) = ((𝐹𝑏)𝐷(𝐹𝑣)))
3184, 5, 6, 259, 262, 264, 266, 268, 270, 272, 274, 276, 286, 295, 298, 304, 308, 313, 317axtg5seg 25164 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑧)𝐷(𝐹𝑢)) = ((𝐹𝑐)𝐷(𝐹𝑣)))
3194, 5, 6, 18, 19, 20, 277, 290, 293, 265, 273f1otrgds 25549 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = ((𝐹𝑧)𝐷(𝐹𝑢)))
3204, 5, 6, 18, 19, 20, 277, 290, 293, 271, 275f1otrgds 25549 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑐𝐸𝑣) = ((𝐹𝑐)𝐷(𝐹𝑣)))
321318, 319, 3203eqtr4d 2654 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))
322321ex 449 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) → (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
323322ralrimiva 2949 . . . . . . . . . . . . 13 ((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) → ∀𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
324323ralrimiva 2949 . . . . . . . . . . . 12 (((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) → ∀𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
325324ralrimiva 2949 . . . . . . . . . . 11 ((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) → ∀𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
326325ralrimiva 2949 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) → ∀𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
327326ralrimiva 2949 . . . . . . . . 9 ((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) → ∀𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
328327ralrimiva 2949 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → ∀𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
329328ralrimiva 2949 . . . . . . 7 ((𝜑𝑥𝐵) → ∀𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
330329ralrimiva 2949 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
331 simp-4l 802 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝜑)
332 simplr 788 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑤𝑃)
333 simprl 790 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤))
334331, 9syl 17 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝐹:𝐵1-1-onto𝑃)
335 f1ocnvfv2 6433 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑤𝑃) → (𝐹‘(𝐹𝑤)) = 𝑤)
336334, 332, 335syl2anc 691 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹‘(𝐹𝑤)) = 𝑤)
337336oveq2d 6565 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))) = ((𝐹𝑥)𝐼𝑤))
338333, 337eleqtrrd 2691 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))))
339331, 22sylan 487 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
340331, 24sylan 487 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
34113ad3antrrr 762 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑥𝐵)
34277ffvelrnda 6267 . . . . . . . . . . . . 13 ((𝜑𝑤𝑃) → (𝐹𝑤) ∈ 𝐵)
343331, 332, 342syl2anc 691 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑤) ∈ 𝐵)
34415ad3antrrr 762 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦𝐵)
3454, 5, 6, 18, 19, 20, 334, 339, 340, 341, 343, 344f1otrgitv 25550 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤)))))
346338, 345mpbird 246 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦 ∈ (𝑥𝐽(𝐹𝑤)))
3474, 5, 6, 18, 19, 20, 334, 339, 340, 344, 343f1otrgds 25549 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))))
348336oveq2d 6565 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))) = ((𝐹𝑦)𝐷𝑤))
349 simprr 792 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))
350347, 348, 3493eqtrd 2648 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
351 simprl 790 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑎𝐵)
352351ad2antrr 758 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑎𝐵)
353 simprr 792 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑏𝐵)
354353ad2antrr 758 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑏𝐵)
3554, 5, 6, 18, 19, 20, 334, 339, 340, 352, 354f1otrgds 25549 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
356350, 355eqtr4d 2647 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))
357 oveq2 6557 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑥𝐽𝑧) = (𝑥𝐽(𝐹𝑤)))
358357eleq2d 2673 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ 𝑦 ∈ (𝑥𝐽(𝐹𝑤))))
359 oveq2 6557 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑦𝐸𝑧) = (𝑦𝐸(𝐹𝑤)))
360359eqeq1d 2612 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → ((𝑦𝐸𝑧) = (𝑎𝐸𝑏) ↔ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)))
361358, 360anbi12d 743 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑤) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
362361adantl 481 . . . . . . . . . . . 12 (((𝜑𝑤𝑃) ∧ 𝑧 = (𝐹𝑤)) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
363342, 362rspcedv 3286 . . . . . . . . . . 11 ((𝜑𝑤𝑃) → ((𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))
364363imp 444 . . . . . . . . . 10 (((𝜑𝑤𝑃) ∧ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
365331, 332, 346, 356, 364syl22anc 1319 . . . . . . . . 9 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3668adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐺 ∈ TarskiG)
36714adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑥) ∈ 𝑃)
36816adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑦) ∈ 𝑃)
36912adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐹:𝐵𝑃)
370369, 351ffvelrnd 6268 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑎) ∈ 𝑃)
371369, 353ffvelrnd 6268 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑏) ∈ 𝑃)
3724, 5, 6, 366, 367, 368, 370, 371axtgsegcon 25163 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑤𝑃 ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏))))
373365, 372r19.29a 3060 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
374373ralrimivva 2954 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
375374ralrimivva 2954 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3763, 330, 375jca32 556 . . . . 5 (𝜑 → (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
37718, 19, 20istrkgcb 25155 . . . . 5 (𝐻 ∈ TarskiGCB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
378376, 377sylibr 223 . . . 4 (𝜑𝐻 ∈ TarskiGCB)
379 f1otrg.l . . . . 5 (𝜑 → (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))
38018, 19, 20istrkgl 25157 . . . . 5 (𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))})))
3813, 379, 380sylanbrc 695 . . . 4 (𝜑𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
382378, 381elind 3760 . . 3 (𝜑𝐻 ∈ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
383258, 382elind 3760 . 2 (𝜑𝐻 ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})))
384 df-trkg 25152 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
385383, 384syl6eleqr 2699 1 (𝜑𝐻 ∈ TarskiG)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∨ w3o 1030   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173  [wsbc 3402   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  𝒫 cpw 4108  {csn 4125  ◡ccnv 5037  ran crn 5039   “ cima 5041   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  Basecbs 15695  distcds 15777  TarskiGcstrkg 25129  TarskiGCcstrkgc 25130  TarskiGBcstrkgb 25131  TarskiGCBcstrkgcb 25132  Itvcitv 25135  LineGclng 25136 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-trkgc 25147  df-trkgb 25148  df-trkgcb 25149  df-trkg 25152 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator