3wlkdlem9 - Metamath Proof Explorer

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

Theorem 3wlkdlem9 30238

Description: Lemma 9 for 3wlkd 30240. (Contributed by AV, 7-Feb-2021.)

**Hypotheses**
Ref	Expression
3wlkd.p	⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩
3wlkd.f	⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩
3wlkd.s	⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))
3wlkd.n	⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))
3wlkd.e	⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))

**Assertion**
Ref	Expression
3wlkdlem9	⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2))))

**Proof of Theorem 3wlkdlem9**
Step	Hyp	Ref	Expression
1		3wlkd.e	. 2 ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))
2		3wlkd.p	. . . 4 ⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩
3		3wlkd.f	. . . 4 ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩
4		3wlkd.s	. . . 4 ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))
5		3wlkd.n	. . . 4 ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))
6	2, 3, 4, 5, 1	3wlkdlem8 30237	. . 3 ⊢ (𝜑 → ((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾 ∧ (𝐹‘2) = 𝐿))
7		fveq2 6840	. . . . . 6 ⊢ ((𝐹‘0) = 𝐽 → (𝐼‘(𝐹‘0)) = (𝐼‘𝐽))
8	7	sseq2d 3954	. . . . 5 ⊢ ((𝐹‘0) = 𝐽 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ↔ {𝐴, 𝐵} ⊆ (𝐼‘𝐽)))
9	8	3ad2ant1 1134	. . . 4 ⊢ (((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾 ∧ (𝐹‘2) = 𝐿) → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ↔ {𝐴, 𝐵} ⊆ (𝐼‘𝐽)))
10		fveq2 6840	. . . . . 6 ⊢ ((𝐹‘1) = 𝐾 → (𝐼‘(𝐹‘1)) = (𝐼‘𝐾))
11	10	sseq2d 3954	. . . . 5 ⊢ ((𝐹‘1) = 𝐾 → ({𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ↔ {𝐵, 𝐶} ⊆ (𝐼‘𝐾)))
12	11	3ad2ant2 1135	. . . 4 ⊢ (((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾 ∧ (𝐹‘2) = 𝐿) → ({𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ↔ {𝐵, 𝐶} ⊆ (𝐼‘𝐾)))
13		fveq2 6840	. . . . . 6 ⊢ ((𝐹‘2) = 𝐿 → (𝐼‘(𝐹‘2)) = (𝐼‘𝐿))
14	13	sseq2d 3954	. . . . 5 ⊢ ((𝐹‘2) = 𝐿 → ({𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2)) ↔ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))
15	14	3ad2ant3 1136	. . . 4 ⊢ (((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾 ∧ (𝐹‘2) = 𝐿) → ({𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2)) ↔ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))
16	9, 12, 15	3anbi123d 1439	. . 3 ⊢ (((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾 ∧ (𝐹‘2) = 𝐿) → (({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2))) ↔ ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))))
17	6, 16	syl 17	. 2 ⊢ (𝜑 → (({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2))) ↔ ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))))
18	1, 17	mpbird 257	1 ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 ⊆ wss 3889 {cpr 4569 ‘cfv 6498 0cc0 11038 1c1 11039 2c2 12236 ⟨“cs3 14804 ⟨“cs4 14805

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-3 12245 df-n0 12438 df-z 12525 df-uz 12789 df-fz 13462 df-fzo 13609 df-hash 14293 df-word 14476 df-concat 14533 df-s1 14559 df-s2 14810 df-s3 14811 df-s4 14812

This theorem is referenced by: 3wlkdlem10 30239

W3C validator