Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem inf3lem5 3468

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 3471 for detailed description.

**Hypotheses**
Ref	Expression
inf3lem.1	⊢ G = {⟨y, z⟩∣z = {w ∈ x∣(w ∩ x) ⊆ y}}
inf3lem.2	⊢ F = (rec(G, ∅) ↾ ω)
inf3lem.3	⊢ A ∈ V
inf3lem.4	⊢ B ∈ V

**Assertion**
Ref	Expression
inf3lem5	⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → ((A ∈ ω ∧ B ∈ A) → (F ‘B) ⊂ (F ‘A)))

Distinct variable group(s): x,y,z,w

**Proof of Theorem inf3lem5**
Step	Hyp	Ref	Expression
1		elnn 2383	. . . 4 ⊢ ((B ∈ A ∧ A ∈ ω) → B ∈ ω)
2	1	ancoms 334	. . 3 ⊢ ((A ∈ ω ∧ B ∈ A) → B ∈ ω)
3		nnord 2381	. . . . . . . . 9 ⊢ (A ∈ ω → Ord A)
4		ordsucss 2320	. . . . . . . . 9 ⊢ (Ord A → (B ∈ A → suc B ⊆ A))
5	3, 4	syl 12	. . . . . . . 8 ⊢ (A ∈ ω → (B ∈ A → suc B ⊆ A))
6	5	adantr 306	. . . . . . 7 ⊢ ((A ∈ ω ∧ B ∈ ω) → (B ∈ A → suc B ⊆ A))
7		fveq2 2832	. . . . . . . . . . . 12 ⊢ (v = suc B → (F ‘v) = (F ‘suc B))
8	7	psseq2d 1565	. . . . . . . . . . 11 ⊢ (v = suc B → ((F ‘B) ⊂ (F ‘v) ↔ (F ‘B) ⊂ (F ‘suc B)))
9	8	imbi2d 464	. . . . . . . . . 10 ⊢ (v = suc B → (((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘v)) ↔ ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘suc B))))
10		fveq2 2832	. . . . . . . . . . . 12 ⊢ (v = u → (F ‘v) = (F ‘u))
11	10	psseq2d 1565	. . . . . . . . . . 11 ⊢ (v = u → ((F ‘B) ⊂ (F ‘v) ↔ (F ‘B) ⊂ (F ‘u)))
12	11	imbi2d 464	. . . . . . . . . 10 ⊢ (v = u → (((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘v)) ↔ ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘u))))
13		fveq2 2832	. . . . . . . . . . . 12 ⊢ (v = suc u → (F ‘v) = (F ‘suc u))
14	13	psseq2d 1565	. . . . . . . . . . 11 ⊢ (v = suc u → ((F ‘B) ⊂ (F ‘v) ↔ (F ‘B) ⊂ (F ‘suc u)))
15	14	imbi2d 464	. . . . . . . . . 10 ⊢ (v = suc u → (((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘v)) ↔ ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘suc u))))
16		fveq2 2832	. . . . . . . . . . . 12 ⊢ (v = A → (F ‘v) = (F ‘A))
17	16	psseq2d 1565	. . . . . . . . . . 11 ⊢ (v = A → ((F ‘B) ⊂ (F ‘v) ↔ (F ‘B) ⊂ (F ‘A)))
18	17	imbi2d 464	. . . . . . . . . 10 ⊢ (v = A → (((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘v)) ↔ ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘A))))
19		peano2b 2388	. . . . . . . . . . 11 ⊢ (B ∈ ω ↔ suc B ∈ ω)
20		inf3lem.1	. . . . . . . . . . . . 13 ⊢ G = {⟨y, z⟩∣z = {w ∈ x∣(w ∩ x) ⊆ y}}
21		inf3lem.2	. . . . . . . . . . . . 13 ⊢ F = (rec(G, ∅) ↾ ω)
22		inf3lem.4	. . . . . . . . . . . . 13 ⊢ B ∈ V
23	20, 21, 22, 22	inf3lem4 3467	. . . . . . . . . . . 12 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → (B ∈ ω → (F ‘B) ⊂ (F ‘suc B)))
24	23	com12 13	. . . . . . . . . . 11 ⊢ (B ∈ ω → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘suc B)))
25	19, 24	sylbir 176	. . . . . . . . . 10 ⊢ (suc B ∈ ω → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘suc B)))
26		visset 1350	. . . . . . . . . . . . . . 15 ⊢ u ∈ V
27	20, 21, 26, 22	inf3lem4 3467	. . . . . . . . . . . . . 14 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → (u ∈ ω → (F ‘u) ⊂ (F ‘suc u)))
28		psstr 1574	. . . . . . . . . . . . . . . 16 ⊢ (((F ‘B) ⊂ (F ‘u) ∧ (F ‘u) ⊂ (F ‘suc u)) → (F ‘B) ⊂ (F ‘suc u))
29	28	exp 291	. . . . . . . . . . . . . . 15 ⊢ ((F ‘B) ⊂ (F ‘u) → ((F ‘u) ⊂ (F ‘suc u) → (F ‘B) ⊂ (F ‘suc u)))
30	29	com12 13	. . . . . . . . . . . . . 14 ⊢ ((F ‘u) ⊂ (F ‘suc u) → ((F ‘B) ⊂ (F ‘u) → (F ‘B) ⊂ (F ‘suc u)))
31	27, 30	syl6 23	. . . . . . . . . . . . 13 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → (u ∈ ω → ((F ‘B) ⊂ (F ‘u) → (F ‘B) ⊂ (F ‘suc u))))
32	31	com12 13	. . . . . . . . . . . 12 ⊢ (u ∈ ω → ((¬ x = ∅ ∧ x ⊆ ∪x) → ((F ‘B) ⊂ (F ‘u) → (F ‘B) ⊂ (F ‘suc u))))
33	32	a2d 15	. . . . . . . . . . 11 ⊢ (u ∈ ω → (((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘u)) → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘suc u))))
34	33	ad2antll 320	. . . . . . . . . 10 ⊢ (((u ∈ ω ∧ suc B ∈ ω) ∧ suc B ⊆ u) → (((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘u)) → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘suc u))))
35	9, 12, 15, 18, 25, 34	findsg 2398	. . . . . . . . 9 ⊢ (((A ∈ ω ∧ suc B ∈ ω) ∧ suc B ⊆ A) → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘A)))
36	35	exp 291	. . . . . . . 8 ⊢ ((A ∈ ω ∧ suc B ∈ ω) → (suc B ⊆ A → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘A))))
37	36, 19	sylan2b 347	. . . . . . 7 ⊢ ((A ∈ ω ∧ B ∈ ω) → (suc B ⊆ A → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘A))))
38	6, 37	syld 27	. . . . . 6 ⊢ ((A ∈ ω ∧ B ∈ ω) → (B ∈ A → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘A))))
39	38	exp 291	. . . . 5 ⊢ (A ∈ ω → (B ∈ ω → (B ∈ A → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘A)))))
40	39	com23 32	. . . 4 ⊢ (A ∈ ω → (B ∈ A → (B ∈ ω → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘A)))))
41	40	imp 277	. . 3 ⊢ ((A ∈ ω ∧ B ∈ A) → (B ∈ ω → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘A))))
42	2, 41	mpd 46	. 2 ⊢ ((A ∈ ω ∧ B ∈ A) → ((¬ x = ∅ ∧ x ⊆ ∪x) → (F ‘B) ⊂ (F ‘A)))
43	42	com12 13	1 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → ((A ∈ ω ∧ B ∈ A) → (F ‘B) ⊂ (F ‘A)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ∧ wa 196 = weq 797 = wceq 1091 ∈ wcel 1092 {crab 1204 Vcvv 1348 ∩ cin 1486 ⊆ wss 1487 ⊂ wpss 1488 ∅c0 1707 ∪cuni 1919 {copab 2055 Ord word 2198 suc csuc 2201 ωcom 2372 ↾ cres 2412 ‘cfv 2422 reccrdg 2969

This theorem is referenced by: inf3lem6 3469

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-fv 2438 df-rdg 2970

metamath.org