fimgmcyclem

		Ref	Expression
	Hypothesis	fimgmcyclem.s	$⊢ φ \to \exists o \in ℕ \exists q \in ℕ (o \neq q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)$
	Assertion	fimgmcyclem	$⊢ φ \to \exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)$

Proof

Step	Hyp	Ref	Expression
1		fimgmcyclem.s	$⊢ φ \to \exists o \in ℕ \exists q \in ℕ (o \neq q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)$
2		simpr	$⊢ (φ \land \exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)) \to \exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)$
3		rexcom	$⊢ \exists r \in ℕ \exists p \in ℕ (p < r \land r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A) \leftrightarrow \exists p \in ℕ \exists r \in ℕ (p < r \land r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A)$
4		eqcom	$⊢ r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A \leftrightarrow p \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A$
5	4	anbi2i	$⊢ (p < r \land r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A) \leftrightarrow (p < r \land p \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A)$
6	5	2rexbii	$⊢ \exists p \in ℕ \exists r \in ℕ (p < r \land r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A) \leftrightarrow \exists p \in ℕ \exists r \in ℕ (p < r \land p \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A)$
7	3 6	sylbb	$⊢ \exists r \in ℕ \exists p \in ℕ (p < r \land r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A) \to \exists p \in ℕ \exists r \in ℕ (p < r \land p \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A)$
8		breq2	$⊢ o = r \to (p < o \leftrightarrow p < r)$
9		oveq1	$⊢ o = r \to o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A$
10	9	eqeq1d	$⊢ o = r \to (o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A \leftrightarrow r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A)$
11	8 10	anbi12d	$⊢ o = r \to ((p < o \land o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A) \leftrightarrow (p < r \land r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A))$
12	11	rexbidv	$⊢ o = r \to (\exists p \in ℕ (p < o \land o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A) \leftrightarrow \exists p \in ℕ (p < r \land r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A))$
13	12	cbvrexvw	$⊢ \exists o \in ℕ \exists p \in ℕ (p < o \land o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A) \leftrightarrow \exists r \in ℕ \exists p \in ℕ (p < r \land r \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A)$
14		breq1	$⊢ o = p \to (o < r \leftrightarrow p < r)$
15		oveq1	$⊢ o = p \to o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A$
16	15	eqeq1d	$⊢ o = p \to (o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A \leftrightarrow p \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A)$
17	14 16	anbi12d	$⊢ o = p \to ((o < r \land o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A) \leftrightarrow (p < r \land p \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A))$
18	17	rexbidv	$⊢ o = p \to (\exists r \in ℕ (o < r \land o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A) \leftrightarrow \exists r \in ℕ (p < r \land p \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A))$
19	18	cbvrexvw	$⊢ \exists o \in ℕ \exists r \in ℕ (o < r \land o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A) \leftrightarrow \exists p \in ℕ \exists r \in ℕ (p < r \land p \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A)$
20	7 13 19	3imtr4i	$⊢ \exists o \in ℕ \exists p \in ℕ (p < o \land o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A) \to \exists o \in ℕ \exists r \in ℕ (o < r \land o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A)$
21		breq1	$⊢ q = p \to (q < o \leftrightarrow p < o)$
22		oveq1	$⊢ q = p \to q \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A$
23	22	eqeq2d	$⊢ q = p \to (o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A \leftrightarrow o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A)$
24	21 23	anbi12d	$⊢ q = p \to ((q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow (p < o \land o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A))$
25	24	cbvrexvw	$⊢ \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow \exists p \in ℕ (p < o \land o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A)$
26	25	rexbii	$⊢ \exists o \in ℕ \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow \exists o \in ℕ \exists p \in ℕ (p < o \land o \underset{˙}{\cdot} A = p \underset{˙}{\cdot} A)$
27		breq2	$⊢ q = r \to (o < q \leftrightarrow o < r)$
28		oveq1	$⊢ q = r \to q \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A$
29	28	eqeq2d	$⊢ q = r \to (o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A \leftrightarrow o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A)$
30	27 29	anbi12d	$⊢ q = r \to ((o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow (o < r \land o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A))$
31	30	cbvrexvw	$⊢ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow \exists r \in ℕ (o < r \land o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A)$
32	31	rexbii	$⊢ \exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow \exists o \in ℕ \exists r \in ℕ (o < r \land o \underset{˙}{\cdot} A = r \underset{˙}{\cdot} A)$
33	20 26 32	3imtr4i	$⊢ \exists o \in ℕ \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \to \exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)$
34	33	adantl	$⊢ (φ \land \exists o \in ℕ \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)) \to \exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)$
35		simpl	$⊢ (o \in ℕ \land q \in ℕ) \to o \in ℕ$
36	35	nnred	$⊢ (o \in ℕ \land q \in ℕ) \to o \in ℝ$
37		simpr	$⊢ (o \in ℕ \land q \in ℕ) \to q \in ℕ$
38	37	nnred	$⊢ (o \in ℕ \land q \in ℕ) \to q \in ℝ$
39	36 38	lttri2d	$⊢ (o \in ℕ \land q \in ℕ) \to (o \neq q \leftrightarrow (o < q \lor q < o))$
40	39	anbi1d	$⊢ (o \in ℕ \land q \in ℕ) \to ((o \neq q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow ((o < q \lor q < o) \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A))$
41		andir	$⊢ ((o < q \lor q < o) \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow ((o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A))$
42	40 41	bitrdi	$⊢ (o \in ℕ \land q \in ℕ) \to ((o \neq q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow ((o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)))$
43	42	2rexbiia	$⊢ \exists o \in ℕ \exists q \in ℕ (o \neq q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow \exists o \in ℕ \exists q \in ℕ ((o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A))$
44		r19.43	$⊢ \exists q \in ℕ ((o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)) \leftrightarrow (\exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A))$
45	44	rexbii	$⊢ \exists o \in ℕ \exists q \in ℕ ((o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)) \leftrightarrow \exists o \in ℕ (\exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A))$
46		r19.43	$⊢ \exists o \in ℕ (\exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)) \leftrightarrow (\exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor \exists o \in ℕ \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A))$
47	43 45 46	3bitri	$⊢ \exists o \in ℕ \exists q \in ℕ (o \neq q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \leftrightarrow (\exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor \exists o \in ℕ \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A))$
48	1 47	sylib	$⊢ φ \to (\exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A) \lor \exists o \in ℕ \exists q \in ℕ (q < o \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A))$
49	2 34 48	mpjaodan	$⊢ φ \to \exists o \in ℕ \exists q \in ℕ (o < q \land o \underset{˙}{\cdot} A = q \underset{˙}{\cdot} A)$

Metamath Proof Explorer

Theorem fimgmcyclem

Proof