SubsetTransitivity Show Code edit
thm (SubsetTransitivity () () (→ (∧ (⊆ A B) (⊆ B C)) (⊆ A C))
A B x Subset
(↔ (⊆ A B) (∀ x (→ (∈ x A) (∈ x B))))
B C x Subset
(↔ (⊆ B C) (∀ x (→ (∈ x B) (∈ x C))))
buildConjunction
(↔ (∧ (⊆ A B) (⊆ B C)) (∧ (∀ x (→ (∈ x A) (∈ x B))) (∀ x (→ (∈ x B) (∈ x C)))))
eliminateBiconditionalReverse
(→ (∧ (⊆ A B) (⊆ B C)) (∧ (∀ x (→ (∈ x A) (∈ x B))) (∀ x (→ (∈ x B) (∈ x C)))))
x
(→ (∈ x A) (∈ x B))
(→ (∈ x B) (∈ x C))
ForAllConjunction
(↔ (∀ x (∧ (→ (∈ x A) (∈ x B)) (→ (∈ x B) (∈ x C)))) (∧ (∀ x (→ (∈ x A) (∈ x B))) (∀ x (→ (∈ x B) (∈ x C)))))
eliminateBiconditionalForward
(→ (∧ (∀ x (→ (∈ x A) (∈ x B))) (∀ x (→ (∈ x B) (∈ x C)))) (∀ x (∧ (→ (∈ x A) (∈ x B)) (→ (∈ x B) (∈ x C)))))
applySyllogism
(→ (∧ (⊆ A B) (⊆ B C)) (∀ x (∧ (→ (∈ x A) (∈ x B)) (→ (∈ x B) (∈ x C)))))
(∈ x A) (∈ x B) (∈ x C) ImplicationTransitivity
(→ (∧ (→ (∈ x A) (∈ x B)) (→ (∈ x B) (∈ x C))) (→ (∈ x A) (∈ x C)))
x addForAll
(→ (∀ x (∧ (→ (∈ x A) (∈ x B)) (→ (∈ x B) (∈ x C)))) (∀ x (→ (∈ x A) (∈ x C))))
applySyllogism
(→ (∧ (⊆ A B) (⊆ B C)) (∀ x (→ (∈ x A) (∈ x C))))
A C x Subset
(↔ (⊆ A C) (∀ x (→ (∈ x A) (∈ x C))))
eliminateBiconditionalForward
(→ (∀ x (→ (∈ x A) (∈ x C))) (⊆ A C))
applySyllogism
(→ (∧ (⊆ A B) (⊆ B C)) (⊆ A C))
)
edit