Metamath Proof Explorer

Theorem dihopelvalcqat

Description: Ordered pair member of the partial isomorphism H for atom argument not under W . TODO: remove .t hypothesis. (Contributed by NM, 30-Mar-2014)

Ref Expression
Hypotheses dihelval2.l ⊢ ≤ ˙ = ≤ K
dihelval2.a ⊢ A = Atoms ⁡ K
dihelval2.h ⊢ H = LHyp ⁡ K
dihelval2.p ⊢ P = oc ⁡ K ⁡ W
dihelval2.t ⊢ T = LTrn ⁡ K ⁡ W
dihelval2.e ⊢ E = TEndo ⁡ K ⁡ W
dihelval2.i ⊢ I = DIsoH ⁡ K ⁡ W
dihelval2.g ⊢ G = ι g ∈ T | g ⁡ P = Q
dihelval2.f ⊢ F ∈ V
dihelval2.s ⊢ S ∈ V
Assertion dihopelvalcqat ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ I ⁡ Q ↔ F = S ⁡ G ∧ S ∈ E

Proof

Step Hyp Ref Expression
1 dihelval2.l ⊢ ≤ ˙ = ≤ K
2 dihelval2.a ⊢ A = Atoms ⁡ K
3 dihelval2.h ⊢ H = LHyp ⁡ K
4 dihelval2.p ⊢ P = oc ⁡ K ⁡ W
5 dihelval2.t ⊢ T = LTrn ⁡ K ⁡ W
6 dihelval2.e ⊢ E = TEndo ⁡ K ⁡ W
7 dihelval2.i ⊢ I = DIsoH ⁡ K ⁡ W
8 dihelval2.g ⊢ G = ι g ∈ T | g ⁡ P = Q
9 dihelval2.f ⊢ F ∈ V
10 dihelval2.s ⊢ S ∈ V
11 eqid ⊢ DIsoC ⁡ K ⁡ W = DIsoC ⁡ K ⁡ W
12 1 2 3 11 7 dihvalcqat ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = DIsoC ⁡ K ⁡ W ⁡ Q
13 12 eleq2d ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ I ⁡ Q ↔ F S ∈ DIsoC ⁡ K ⁡ W ⁡ Q
14 1 2 3 4 5 6 11 8 9 10 dicopelval2 ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ DIsoC ⁡ K ⁡ W ⁡ Q ↔ F = S ⁡ G ∧ S ∈ E
15 13 14 bitrd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ I ⁡ Q ↔ F = S ⁡ G ∧ S ∈ E