Theorem ltfintri 4467

Description: Trichotomy law for finite less than. (Contributed by SF, 29-Jan-2015.)

Assertion

Ref	Expression
ltfintri	⊢ ((M ∈ Nn ∧ N ∈ Nn ∧ M ≠ ∅) → (⟪M, N⟫ ∈ <fin ∨ M = N ∨ ⟪N, M⟫ ∈ <fin ))

Proof of Theorem ltfintri

Dummy variables m n k p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opkeq2 4061	. . . . . . . 8 ⊢ (n = N → ⟪M, n⟫ = ⟪M, N⟫)
2	1	eleq1d 2419	. . . . . . 7 ⊢ (n = N → (⟪M, n⟫ ∈ <fin ↔ ⟪M, N⟫ ∈ <fin ))
3		eqeq2 2362	. . . . . . 7 ⊢ (n = N → (M = n ↔ M = N))
4		opkeq1 4060	. . . . . . . 8 ⊢ (n = N → ⟪n, M⟫ = ⟪N, M⟫)
5	4	eleq1d 2419	. . . . . . 7 ⊢ (n = N → (⟪n, M⟫ ∈ <fin ↔ ⟪N, M⟫ ∈ <fin ))
6	2, 3, 5	3orbi123d 1251	. . . . . 6 ⊢ (n = N → ((⟪M, n⟫ ∈ <fin ∨ M = n ∨ ⟪n, M⟫ ∈ <fin ) ↔ (⟪M, N⟫ ∈ <fin ∨ M = N ∨ ⟪N, M⟫ ∈ <fin )))
7	6	imbi2d 307	. . . . 5 ⊢ (n = N → ((M ≠ ∅ → (⟪M, n⟫ ∈ <fin ∨ M = n ∨ ⟪n, M⟫ ∈ <fin )) ↔ (M ≠ ∅ → (⟪M, N⟫ ∈ <fin ∨ M = N ∨ ⟪N, M⟫ ∈ <fin ))))
8	7	imbi2d 307	. . . 4 ⊢ (n = N → ((M ∈ Nn → (M ≠ ∅ → (⟪M, n⟫ ∈ <fin ∨ M = n ∨ ⟪n, M⟫ ∈ <fin ))) ↔ (M ∈ Nn → (M ≠ ∅ → (⟪M, N⟫ ∈ <fin ∨ M = N ∨ ⟪N, M⟫ ∈ <fin )))))
9		ltfintrilem1 4466	. . . . . 6 ⊢ {k ∣ (n ∈ Nn → (k ≠ ∅ → (⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin )))} ∈ V
10		neeq1 2525	. . . . . . . 8 ⊢ (k = 0c → (k ≠ ∅ ↔ 0c ≠ ∅))
11		opkeq1 4060	. . . . . . . . . 10 ⊢ (k = 0c → ⟪k, n⟫ = ⟪0c, n⟫)
12	11	eleq1d 2419	. . . . . . . . 9 ⊢ (k = 0c → (⟪k, n⟫ ∈ <fin ↔ ⟪0c, n⟫ ∈ <fin ))
13		eqeq1 2359	. . . . . . . . 9 ⊢ (k = 0c → (k = n ↔ 0c = n))
14		opkeq2 4061	. . . . . . . . . 10 ⊢ (k = 0c → ⟪n, k⟫ = ⟪n, 0c⟫)
15	14	eleq1d 2419	. . . . . . . . 9 ⊢ (k = 0c → (⟪n, k⟫ ∈ <fin ↔ ⟪n, 0c⟫ ∈ <fin ))
16	12, 13, 15	3orbi123d 1251	. . . . . . . 8 ⊢ (k = 0c → ((⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin ) ↔ (⟪0c, n⟫ ∈ <fin ∨ 0c = n ∨ ⟪n, 0c⟫ ∈ <fin )))
17	10, 16	imbi12d 311	. . . . . . 7 ⊢ (k = 0c → ((k ≠ ∅ → (⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin )) ↔ (0c ≠ ∅ → (⟪0c, n⟫ ∈ <fin ∨ 0c = n ∨ ⟪n, 0c⟫ ∈ <fin ))))
18	17	imbi2d 307	. . . . . 6 ⊢ (k = 0c → ((n ∈ Nn → (k ≠ ∅ → (⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin ))) ↔ (n ∈ Nn → (0c ≠ ∅ → (⟪0c, n⟫ ∈ <fin ∨ 0c = n ∨ ⟪n, 0c⟫ ∈ <fin )))))
19		neeq1 2525	. . . . . . . 8 ⊢ (k = m → (k ≠ ∅ ↔ m ≠ ∅))
20		opkeq1 4060	. . . . . . . . . 10 ⊢ (k = m → ⟪k, n⟫ = ⟪m, n⟫)
21	20	eleq1d 2419	. . . . . . . . 9 ⊢ (k = m → (⟪k, n⟫ ∈ <fin ↔ ⟪m, n⟫ ∈ <fin ))
22		eqeq1 2359	. . . . . . . . 9 ⊢ (k = m → (k = n ↔ m = n))
23		opkeq2 4061	. . . . . . . . . 10 ⊢ (k = m → ⟪n, k⟫ = ⟪n, m⟫)
24	23	eleq1d 2419	. . . . . . . . 9 ⊢ (k = m → (⟪n, k⟫ ∈ <fin ↔ ⟪n, m⟫ ∈ <fin ))
25	21, 22, 24	3orbi123d 1251	. . . . . . . 8 ⊢ (k = m → ((⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin ) ↔ (⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin )))
26	19, 25	imbi12d 311	. . . . . . 7 ⊢ (k = m → ((k ≠ ∅ → (⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin )) ↔ (m ≠ ∅ → (⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin ))))
27	26	imbi2d 307	. . . . . 6 ⊢ (k = m → ((n ∈ Nn → (k ≠ ∅ → (⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin ))) ↔ (n ∈ Nn → (m ≠ ∅ → (⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin )))))
28		neeq1 2525	. . . . . . . 8 ⊢ (k = (m +c 1c) → (k ≠ ∅ ↔ (m +c 1c) ≠ ∅))
29		opkeq1 4060	. . . . . . . . . 10 ⊢ (k = (m +c 1c) → ⟪k, n⟫ = ⟪(m +c 1c), n⟫)
30	29	eleq1d 2419	. . . . . . . . 9 ⊢ (k = (m +c 1c) → (⟪k, n⟫ ∈ <fin ↔ ⟪(m +c 1c), n⟫ ∈ <fin ))
31		eqeq1 2359	. . . . . . . . 9 ⊢ (k = (m +c 1c) → (k = n ↔ (m +c 1c) = n))
32		opkeq2 4061	. . . . . . . . . 10 ⊢ (k = (m +c 1c) → ⟪n, k⟫ = ⟪n, (m +c 1c)⟫)
33	32	eleq1d 2419	. . . . . . . . 9 ⊢ (k = (m +c 1c) → (⟪n, k⟫ ∈ <fin ↔ ⟪n, (m +c 1c)⟫ ∈ <fin ))
34	30, 31, 33	3orbi123d 1251	. . . . . . . 8 ⊢ (k = (m +c 1c) → ((⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin ) ↔ (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin )))
35	28, 34	imbi12d 311	. . . . . . 7 ⊢ (k = (m +c 1c) → ((k ≠ ∅ → (⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin )) ↔ ((m +c 1c) ≠ ∅ → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin ))))
36	35	imbi2d 307	. . . . . 6 ⊢ (k = (m +c 1c) → ((n ∈ Nn → (k ≠ ∅ → (⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin ))) ↔ (n ∈ Nn → ((m +c 1c) ≠ ∅ → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin )))))
37		neeq1 2525	. . . . . . . 8 ⊢ (k = M → (k ≠ ∅ ↔ M ≠ ∅))
38		opkeq1 4060	. . . . . . . . . 10 ⊢ (k = M → ⟪k, n⟫ = ⟪M, n⟫)
39	38	eleq1d 2419	. . . . . . . . 9 ⊢ (k = M → (⟪k, n⟫ ∈ <fin ↔ ⟪M, n⟫ ∈ <fin ))
40		eqeq1 2359	. . . . . . . . 9 ⊢ (k = M → (k = n ↔ M = n))
41		opkeq2 4061	. . . . . . . . . 10 ⊢ (k = M → ⟪n, k⟫ = ⟪n, M⟫)
42	41	eleq1d 2419	. . . . . . . . 9 ⊢ (k = M → (⟪n, k⟫ ∈ <fin ↔ ⟪n, M⟫ ∈ <fin ))
43	39, 40, 42	3orbi123d 1251	. . . . . . . 8 ⊢ (k = M → ((⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin ) ↔ (⟪M, n⟫ ∈ <fin ∨ M = n ∨ ⟪n, M⟫ ∈ <fin )))
44	37, 43	imbi12d 311	. . . . . . 7 ⊢ (k = M → ((k ≠ ∅ → (⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin )) ↔ (M ≠ ∅ → (⟪M, n⟫ ∈ <fin ∨ M = n ∨ ⟪n, M⟫ ∈ <fin ))))
45	44	imbi2d 307	. . . . . 6 ⊢ (k = M → ((n ∈ Nn → (k ≠ ∅ → (⟪k, n⟫ ∈ <fin ∨ k = n ∨ ⟪n, k⟫ ∈ <fin ))) ↔ (n ∈ Nn → (M ≠ ∅ → (⟪M, n⟫ ∈ <fin ∨ M = n ∨ ⟪n, M⟫ ∈ <fin )))))
46		0cminle 4462	. . . . . . . . . 10 ⊢ (n ∈ Nn → ⟪0c, n⟫ ∈ ≤fin )
47	46	adantr 451	. . . . . . . . 9 ⊢ ((n ∈ Nn ∧ 0c ≠ ∅) → ⟪0c, n⟫ ∈ ≤fin )
48		0cex 4393	. . . . . . . . . . 11 ⊢ 0c ∈ V
49		lefinlteq 4464	. . . . . . . . . . 11 ⊢ ((0c ∈ V ∧ n ∈ Nn ∧ 0c ≠ ∅) → (⟪0c, n⟫ ∈ ≤fin ↔ (⟪0c, n⟫ ∈ <fin ∨ 0c = n)))
50	48, 49	mp3an1 1264	. . . . . . . . . 10 ⊢ ((n ∈ Nn ∧ 0c ≠ ∅) → (⟪0c, n⟫ ∈ ≤fin ↔ (⟪0c, n⟫ ∈ <fin ∨ 0c = n)))
51		orcom 376	. . . . . . . . . 10 ⊢ ((⟪0c, n⟫ ∈ <fin ∨ 0c = n) ↔ (0c = n ∨ ⟪0c, n⟫ ∈ <fin ))
52	50, 51	syl6bb 252	. . . . . . . . 9 ⊢ ((n ∈ Nn ∧ 0c ≠ ∅) → (⟪0c, n⟫ ∈ ≤fin ↔ (0c = n ∨ ⟪0c, n⟫ ∈ <fin )))
53	47, 52	mpbid 201	. . . . . . . 8 ⊢ ((n ∈ Nn ∧ 0c ≠ ∅) → (0c = n ∨ ⟪0c, n⟫ ∈ <fin ))
54		3mix2 1125	. . . . . . . . 9 ⊢ (0c = n → (⟪0c, n⟫ ∈ <fin ∨ 0c = n ∨ ⟪n, 0c⟫ ∈ <fin ))
55		3mix1 1124	. . . . . . . . 9 ⊢ (⟪0c, n⟫ ∈ <fin → (⟪0c, n⟫ ∈ <fin ∨ 0c = n ∨ ⟪n, 0c⟫ ∈ <fin ))
56	54, 55	jaoi 368	. . . . . . . 8 ⊢ ((0c = n ∨ ⟪0c, n⟫ ∈ <fin ) → (⟪0c, n⟫ ∈ <fin ∨ 0c = n ∨ ⟪n, 0c⟫ ∈ <fin ))
57	53, 56	syl 15	. . . . . . 7 ⊢ ((n ∈ Nn ∧ 0c ≠ ∅) → (⟪0c, n⟫ ∈ <fin ∨ 0c = n ∨ ⟪n, 0c⟫ ∈ <fin ))
58	57	ex 423	. . . . . 6 ⊢ (n ∈ Nn → (0c ≠ ∅ → (⟪0c, n⟫ ∈ <fin ∨ 0c = n ∨ ⟪n, 0c⟫ ∈ <fin )))
59		addcnnul 4454	. . . . . . . . . . . . 13 ⊢ ((m +c 1c) ≠ ∅ → (m ≠ ∅ ∧ 1c ≠ ∅))
60	59	simpld 445	. . . . . . . . . . . 12 ⊢ ((m +c 1c) ≠ ∅ → m ≠ ∅)
61	60	3ad2ant3 978	. . . . . . . . . . 11 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → m ≠ ∅)
62		addc32 4417	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((m +c p) +c 1c) = ((m +c 1c) +c p)
63	62	eqeq2i 2363	. . . . . . . . . . . . . . . . . . 19 ⊢ (n = ((m +c p) +c 1c) ↔ n = ((m +c 1c) +c p))
64	63	rexbii 2640	. . . . . . . . . . . . . . . . . 18 ⊢ (∃p ∈ Nn n = ((m +c p) +c 1c) ↔ ∃p ∈ Nn n = ((m +c 1c) +c p))
65	64	biimpi 186	. . . . . . . . . . . . . . . . 17 ⊢ (∃p ∈ Nn n = ((m +c p) +c 1c) → ∃p ∈ Nn n = ((m +c 1c) +c p))
66	65	adantl 452	. . . . . . . . . . . . . . . 16 ⊢ ((m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)) → ∃p ∈ Nn n = ((m +c 1c) +c p))
67	66	a1i 10	. . . . . . . . . . . . . . 15 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → ((m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)) → ∃p ∈ Nn n = ((m +c 1c) +c p)))
68		opkltfing 4450	. . . . . . . . . . . . . . . 16 ⊢ ((m ∈ Nn ∧ n ∈ Nn ) → (⟪m, n⟫ ∈ <fin ↔ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c))))
69	68	3adant3 975	. . . . . . . . . . . . . . 15 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (⟪m, n⟫ ∈ <fin ↔ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c))))
70		simp1 955	. . . . . . . . . . . . . . . . 17 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → m ∈ Nn )
71		peano2 4404	. . . . . . . . . . . . . . . . 17 ⊢ (m ∈ Nn → (m +c 1c) ∈ Nn )
72	70, 71	syl 15	. . . . . . . . . . . . . . . 16 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (m +c 1c) ∈ Nn )
73		simp2 956	. . . . . . . . . . . . . . . 16 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → n ∈ Nn )
74		opklefing 4449	. . . . . . . . . . . . . . . 16 ⊢ (((m +c 1c) ∈ Nn ∧ n ∈ Nn ) → (⟪(m +c 1c), n⟫ ∈ ≤fin ↔ ∃p ∈ Nn n = ((m +c 1c) +c p)))
75	72, 73, 74	syl2anc 642	. . . . . . . . . . . . . . 15 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (⟪(m +c 1c), n⟫ ∈ ≤fin ↔ ∃p ∈ Nn n = ((m +c 1c) +c p)))
76	67, 69, 75	3imtr4d 259	. . . . . . . . . . . . . 14 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (⟪m, n⟫ ∈ <fin → ⟪(m +c 1c), n⟫ ∈ ≤fin ))
77		lefinlteq 4464	. . . . . . . . . . . . . . 15 ⊢ (((m +c 1c) ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (⟪(m +c 1c), n⟫ ∈ ≤fin ↔ (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n)))
78	71, 77	syl3an1 1215	. . . . . . . . . . . . . 14 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (⟪(m +c 1c), n⟫ ∈ ≤fin ↔ (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n)))
79	76, 78	sylibd 205	. . . . . . . . . . . . 13 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (⟪m, n⟫ ∈ <fin → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n)))
80		3mix1 1124	. . . . . . . . . . . . . 14 ⊢ (⟪(m +c 1c), n⟫ ∈ <fin → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin ))
81		3mix2 1125	. . . . . . . . . . . . . 14 ⊢ ((m +c 1c) = n → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin ))
82	80, 81	jaoi 368	. . . . . . . . . . . . 13 ⊢ ((⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n) → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin ))
83	79, 82	syl6 29	. . . . . . . . . . . 12 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (⟪m, n⟫ ∈ <fin → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin )))
84		ltfinp1 4463	. . . . . . . . . . . . . . . 16 ⊢ ((m ∈ Nn ∧ m ≠ ∅) → ⟪m, (m +c 1c)⟫ ∈ <fin )
85	60, 84	sylan2 460	. . . . . . . . . . . . . . 15 ⊢ ((m ∈ Nn ∧ (m +c 1c) ≠ ∅) → ⟪m, (m +c 1c)⟫ ∈ <fin )
86	85	3adant2 974	. . . . . . . . . . . . . 14 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → ⟪m, (m +c 1c)⟫ ∈ <fin )
87		opkeq1 4060	. . . . . . . . . . . . . . 15 ⊢ (m = n → ⟪m, (m +c 1c)⟫ = ⟪n, (m +c 1c)⟫)
88	87	eleq1d 2419	. . . . . . . . . . . . . 14 ⊢ (m = n → (⟪m, (m +c 1c)⟫ ∈ <fin ↔ ⟪n, (m +c 1c)⟫ ∈ <fin ))
89	86, 88	syl5ibcom 211	. . . . . . . . . . . . 13 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (m = n → ⟪n, (m +c 1c)⟫ ∈ <fin ))
90		3mix3 1126	. . . . . . . . . . . . 13 ⊢ (⟪n, (m +c 1c)⟫ ∈ <fin → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin ))
91	89, 90	syl6 29	. . . . . . . . . . . 12 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (m = n → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin )))
92		ltfintr 4460	. . . . . . . . . . . . . . 15 ⊢ ((n ∈ Nn ∧ m ∈ Nn ∧ (m +c 1c) ∈ Nn ) → ((⟪n, m⟫ ∈ <fin ∧ ⟪m, (m +c 1c)⟫ ∈ <fin ) → ⟪n, (m +c 1c)⟫ ∈ <fin ))
93	73, 70, 72, 92	syl3anc 1182	. . . . . . . . . . . . . 14 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → ((⟪n, m⟫ ∈ <fin ∧ ⟪m, (m +c 1c)⟫ ∈ <fin ) → ⟪n, (m +c 1c)⟫ ∈ <fin ))
94	86, 93	mpan2d 655	. . . . . . . . . . . . 13 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (⟪n, m⟫ ∈ <fin → ⟪n, (m +c 1c)⟫ ∈ <fin ))
95	94, 90	syl6 29	. . . . . . . . . . . 12 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → (⟪n, m⟫ ∈ <fin → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin )))
96	83, 91, 95	3jaod 1246	. . . . . . . . . . 11 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → ((⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin ) → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin )))
97	61, 96	embantd 50	. . . . . . . . . 10 ⊢ ((m ∈ Nn ∧ n ∈ Nn ∧ (m +c 1c) ≠ ∅) → ((m ≠ ∅ → (⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin )) → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin )))
98	97	3expia 1153	. . . . . . . . 9 ⊢ ((m ∈ Nn ∧ n ∈ Nn ) → ((m +c 1c) ≠ ∅ → ((m ≠ ∅ → (⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin )) → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin ))))
99	98	com23 72	. . . . . . . 8 ⊢ ((m ∈ Nn ∧ n ∈ Nn ) → ((m ≠ ∅ → (⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin )) → ((m +c 1c) ≠ ∅ → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin ))))
100	99	ex 423	. . . . . . 7 ⊢ (m ∈ Nn → (n ∈ Nn → ((m ≠ ∅ → (⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin )) → ((m +c 1c) ≠ ∅ → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin )))))
101	100	a2d 23	. . . . . 6 ⊢ (m ∈ Nn → ((n ∈ Nn → (m ≠ ∅ → (⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin ))) → (n ∈ Nn → ((m +c 1c) ≠ ∅ → (⟪(m +c 1c), n⟫ ∈ <fin ∨ (m +c 1c) = n ∨ ⟪n, (m +c 1c)⟫ ∈ <fin )))))
102	9, 18, 27, 36, 45, 58, 101	finds 4412	. . . . 5 ⊢ (M ∈ Nn → (n ∈ Nn → (M ≠ ∅ → (⟪M, n⟫ ∈ <fin ∨ M = n ∨ ⟪n, M⟫ ∈ <fin ))))
103	102	com12 27	. . . 4 ⊢ (n ∈ Nn → (M ∈ Nn → (M ≠ ∅ → (⟪M, n⟫ ∈ <fin ∨ M = n ∨ ⟪n, M⟫ ∈ <fin ))))
104	8, 103	vtoclga 2921	. . 3 ⊢ (N ∈ Nn → (M ∈ Nn → (M ≠ ∅ → (⟪M, N⟫ ∈ <fin ∨ M = N ∨ ⟪N, M⟫ ∈ <fin ))))
105	104	com12 27	. 2 ⊢ (M ∈ Nn → (N ∈ Nn → (M ≠ ∅ → (⟪M, N⟫ ∈ <fin ∨ M = N ∨ ⟪N, M⟫ ∈ <fin ))))
106	105	3imp 1145	1 ⊢ ((M ∈ Nn ∧ N ∈ Nn ∧ M ≠ ∅) → (⟪M, N⟫ ∈ <fin ∨ M = N ∨ ⟪N, M⟫ ∈ <fin ))

Syntax hints:   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∨ w3o 933   ∧ w3a 934   = wceq 1642   ∈ wcel 1710   ≠ wne 2517  ∃wrex 2616  Vcvv 2860  ∅c0 3551  ⟪copk 4058  1_cc1c 4135   Nn cnnc 4374  0_cc0c 4375   +_c cplc 4376   ≤_fin clefin 4433   <_fin cltfin 4434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-0c 4378  df-addc 4379  df-nnc 4380  df-lefin 4441  df-ltfin 4442

This theorem is referenced by:  lenltfin  4470  tfinltfin  4502  sfin111  4537