Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  5oalem7 Structured version   Visualization version   GIF version

Theorem 5oalem7 29532
 Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) TODO: replace uses of ee4anv 2362 with 4exdistrv 1958 as in 3oalem3 29536. (New usage is discouraged.)
Hypotheses
Ref Expression
5oalem5.1 𝐴S
5oalem5.2 𝐵S
5oalem5.3 𝐶S
5oalem5.4 𝐷S
5oalem5.5 𝐹S
5oalem5.6 𝐺S
5oalem5.7 𝑅S
5oalem5.8 𝑆S
Assertion
Ref Expression
5oalem7 (((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)) ∩ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆))) ⊆ (𝐵 + (𝐴 ∩ (𝐶 + ((((𝐴 + 𝐶) ∩ (𝐵 + 𝐷)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)))) ∩ ((((𝐴 + 𝐹) ∩ (𝐵 + 𝐺)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))) + (((𝐶 + 𝐹) ∩ (𝐷 + 𝐺)) ∩ (((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))))))))

Proof of Theorem 5oalem7
Dummy variables 𝑓 𝑔 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ee4anv 2362 . . . 4 (∃𝑥𝑦𝑓𝑔(∃𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ ∃𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) ↔ (∃𝑥𝑦𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ ∃𝑓𝑔𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))))
2 exrot4 2171 . . . . . 6 (∃𝑧𝑤𝑓𝑔𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) ↔ ∃𝑓𝑔𝑧𝑤𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))))
3 ee4anv 2362 . . . . . . 7 (∃𝑧𝑤𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) ↔ (∃𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ ∃𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))))
432exbii 1851 . . . . . 6 (∃𝑓𝑔𝑧𝑤𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) ↔ ∃𝑓𝑔(∃𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ ∃𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))))
52, 4bitri 278 . . . . 5 (∃𝑧𝑤𝑓𝑔𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) ↔ ∃𝑓𝑔(∃𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ ∃𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))))
652exbii 1851 . . . 4 (∃𝑥𝑦𝑧𝑤𝑓𝑔𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) ↔ ∃𝑥𝑦𝑓𝑔(∃𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ ∃𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))))
7 elin 3875 . . . . 5 ( ∈ (((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)) ∩ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆))) ↔ ( ∈ ((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)) ∧ ∈ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆))))
8 5oalem5.1 . . . . . . . . . 10 𝐴S
9 5oalem5.2 . . . . . . . . . 10 𝐵S
108, 9shseli 29188 . . . . . . . . 9 ( ∈ (𝐴 + 𝐵) ↔ ∃𝑥𝐴𝑦𝐵 = (𝑥 + 𝑦))
11 r2ex 3228 . . . . . . . . 9 (∃𝑥𝐴𝑦𝐵 = (𝑥 + 𝑦) ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)))
1210, 11bitri 278 . . . . . . . 8 ( ∈ (𝐴 + 𝐵) ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)))
13 5oalem5.3 . . . . . . . . . 10 𝐶S
14 5oalem5.4 . . . . . . . . . 10 𝐷S
1513, 14shseli 29188 . . . . . . . . 9 ( ∈ (𝐶 + 𝐷) ↔ ∃𝑧𝐶𝑤𝐷 = (𝑧 + 𝑤))
16 r2ex 3228 . . . . . . . . 9 (∃𝑧𝐶𝑤𝐷 = (𝑧 + 𝑤) ↔ ∃𝑧𝑤((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤)))
1715, 16bitri 278 . . . . . . . 8 ( ∈ (𝐶 + 𝐷) ↔ ∃𝑧𝑤((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤)))
1812, 17anbi12i 630 . . . . . . 7 (( ∈ (𝐴 + 𝐵) ∧ ∈ (𝐶 + 𝐷)) ↔ (∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ∃𝑧𝑤((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))))
19 elin 3875 . . . . . . 7 ( ∈ ((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)) ↔ ( ∈ (𝐴 + 𝐵) ∧ ∈ (𝐶 + 𝐷)))
20 ee4anv 2362 . . . . . . 7 (∃𝑥𝑦𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ↔ (∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ∃𝑧𝑤((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))))
2118, 19, 203bitr4ri 308 . . . . . 6 (∃𝑥𝑦𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ↔ ∈ ((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)))
22 5oalem5.5 . . . . . . . . . 10 𝐹S
23 5oalem5.6 . . . . . . . . . 10 𝐺S
2422, 23shseli 29188 . . . . . . . . 9 ( ∈ (𝐹 + 𝐺) ↔ ∃𝑓𝐹𝑔𝐺 = (𝑓 + 𝑔))
25 r2ex 3228 . . . . . . . . 9 (∃𝑓𝐹𝑔𝐺 = (𝑓 + 𝑔) ↔ ∃𝑓𝑔((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)))
2624, 25bitri 278 . . . . . . . 8 ( ∈ (𝐹 + 𝐺) ↔ ∃𝑓𝑔((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)))
27 5oalem5.7 . . . . . . . . . 10 𝑅S
28 5oalem5.8 . . . . . . . . . 10 𝑆S
2927, 28shseli 29188 . . . . . . . . 9 ( ∈ (𝑅 + 𝑆) ↔ ∃𝑣𝑅𝑢𝑆 = (𝑣 + 𝑢))
30 r2ex 3228 . . . . . . . . 9 (∃𝑣𝑅𝑢𝑆 = (𝑣 + 𝑢) ↔ ∃𝑣𝑢((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))
3129, 30bitri 278 . . . . . . . 8 ( ∈ (𝑅 + 𝑆) ↔ ∃𝑣𝑢((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))
3226, 31anbi12i 630 . . . . . . 7 (( ∈ (𝐹 + 𝐺) ∧ ∈ (𝑅 + 𝑆)) ↔ (∃𝑓𝑔((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ∃𝑣𝑢((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢))))
33 elin 3875 . . . . . . 7 ( ∈ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆)) ↔ ( ∈ (𝐹 + 𝐺) ∧ ∈ (𝑅 + 𝑆)))
34 ee4anv 2362 . . . . . . 7 (∃𝑓𝑔𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢))) ↔ (∃𝑓𝑔((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ∃𝑣𝑢((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢))))
3532, 33, 343bitr4ri 308 . . . . . 6 (∃𝑓𝑔𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢))) ↔ ∈ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆)))
3621, 35anbi12i 630 . . . . 5 ((∃𝑥𝑦𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ ∃𝑓𝑔𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) ↔ ( ∈ ((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)) ∧ ∈ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆))))
377, 36bitr4i 281 . . . 4 ( ∈ (((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)) ∩ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆))) ↔ (∃𝑥𝑦𝑧𝑤(((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ ∃𝑓𝑔𝑣𝑢(((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))))
381, 6, 373bitr4ri 308 . . 3 ( ∈ (((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)) ∩ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆))) ↔ ∃𝑥𝑦𝑧𝑤𝑓𝑔𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))))
398, 9, 13, 14, 22, 23, 27, 285oalem6 29531 . . . . . . 7 (((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) → ∈ (𝐵 + (𝐴 ∩ (𝐶 + ((((𝐴 + 𝐶) ∩ (𝐵 + 𝐷)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)))) ∩ ((((𝐴 + 𝐹) ∩ (𝐵 + 𝐺)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))) + (((𝐶 + 𝐹) ∩ (𝐷 + 𝐺)) ∩ (((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆))))))))))
4039exlimivv 1934 . . . . . 6 (∃𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) → ∈ (𝐵 + (𝐴 ∩ (𝐶 + ((((𝐴 + 𝐶) ∩ (𝐵 + 𝐷)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)))) ∩ ((((𝐴 + 𝐹) ∩ (𝐵 + 𝐺)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))) + (((𝐶 + 𝐹) ∩ (𝐷 + 𝐺)) ∩ (((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆))))))))))
4140exlimivv 1934 . . . . 5 (∃𝑓𝑔𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) → ∈ (𝐵 + (𝐴 ∩ (𝐶 + ((((𝐴 + 𝐶) ∩ (𝐵 + 𝐷)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)))) ∩ ((((𝐴 + 𝐹) ∩ (𝐵 + 𝐺)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))) + (((𝐶 + 𝐹) ∩ (𝐷 + 𝐺)) ∩ (((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆))))))))))
4241exlimivv 1934 . . . 4 (∃𝑧𝑤𝑓𝑔𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) → ∈ (𝐵 + (𝐴 ∩ (𝐶 + ((((𝐴 + 𝐶) ∩ (𝐵 + 𝐷)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)))) ∩ ((((𝐴 + 𝐹) ∩ (𝐵 + 𝐺)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))) + (((𝐶 + 𝐹) ∩ (𝐷 + 𝐺)) ∩ (((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆))))))))))
4342exlimivv 1934 . . 3 (∃𝑥𝑦𝑧𝑤𝑓𝑔𝑣𝑢((((𝑥𝐴𝑦𝐵) ∧ = (𝑥 + 𝑦)) ∧ ((𝑧𝐶𝑤𝐷) ∧ = (𝑧 + 𝑤))) ∧ (((𝑓𝐹𝑔𝐺) ∧ = (𝑓 + 𝑔)) ∧ ((𝑣𝑅𝑢𝑆) ∧ = (𝑣 + 𝑢)))) → ∈ (𝐵 + (𝐴 ∩ (𝐶 + ((((𝐴 + 𝐶) ∩ (𝐵 + 𝐷)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)))) ∩ ((((𝐴 + 𝐹) ∩ (𝐵 + 𝐺)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))) + (((𝐶 + 𝐹) ∩ (𝐷 + 𝐺)) ∩ (((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆))))))))))
4438, 43sylbi 220 . 2 ( ∈ (((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)) ∩ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆))) → ∈ (𝐵 + (𝐴 ∩ (𝐶 + ((((𝐴 + 𝐶) ∩ (𝐵 + 𝐷)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)))) ∩ ((((𝐴 + 𝐹) ∩ (𝐵 + 𝐺)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))) + (((𝐶 + 𝐹) ∩ (𝐷 + 𝐺)) ∩ (((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆))))))))))
4544ssriv 3897 1 (((𝐴 + 𝐵) ∩ (𝐶 + 𝐷)) ∩ ((𝐹 + 𝐺) ∩ (𝑅 + 𝑆))) ⊆ (𝐵 + (𝐴 ∩ (𝐶 + ((((𝐴 + 𝐶) ∩ (𝐵 + 𝐷)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)))) ∩ ((((𝐴 + 𝐹) ∩ (𝐵 + 𝐺)) ∩ (((𝐴 + 𝑅) ∩ (𝐵 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))) + (((𝐶 + 𝐹) ∩ (𝐷 + 𝐺)) ∩ (((𝐶 + 𝑅) ∩ (𝐷 + 𝑆)) + ((𝐹 + 𝑅) ∩ (𝐺 + 𝑆)))))))))
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112  ∃wrex 3072   ∩ cin 3858   ⊆ wss 3859  (class class class)co 7148   +ℎ cva 28792   Sℋ csh 28800   +ℋ cph 28803 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-resscn 10622  ax-1cn 10623  ax-icn 10624  ax-addcl 10625  ax-addrcl 10626  ax-mulcl 10627  ax-mulrcl 10628  ax-mulcom 10629  ax-addass 10630  ax-mulass 10631  ax-distr 10632  ax-i2m1 10633  ax-1ne0 10634  ax-1rid 10635  ax-rnegex 10636  ax-rrecex 10637  ax-cnre 10638  ax-pre-lttri 10639  ax-pre-lttrn 10640  ax-pre-ltadd 10641  ax-hilex 28871  ax-hfvadd 28872  ax-hvcom 28873  ax-hvass 28874  ax-hv0cl 28875  ax-hvaddid 28876  ax-hfvmul 28877  ax-hvmulid 28878  ax-hvmulass 28879  ax-hvdistr1 28880  ax-hvdistr2 28881  ax-hvmul0 28882 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-tp 4525  df-op 4527  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7578  df-wrecs 7955  df-recs 8016  df-rdg 8054  df-er 8297  df-map 8416  df-en 8526  df-dom 8527  df-sdom 8528  df-pnf 10705  df-mnf 10706  df-ltxr 10708  df-sub 10900  df-neg 10901  df-nn 11665  df-grpo 28365  df-ablo 28417  df-hvsub 28843  df-hlim 28844  df-sh 29079  df-ch 29093  df-shs 29180 This theorem is referenced by:  5oai  29533
 Copyright terms: Public domain W3C validator