Theorem inf3lem6 3469

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
inf3lem6	⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → F:ω–1-1→℘x)

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

Proof of Theorem inf3lem6

Step	Hyp	Ref	Expression
1		inf3lem.1	. . . . . . . . . . . . . 14 ⊢ G = {⟨y, z⟩∣z = {w ∈ x∣(w ∩ x) ⊆ y}}
2		inf3lem.2	. . . . . . . . . . . . . 14 ⊢ F = (rec(G, ∅) ↾ ω)
3		visset 1350	. . . . . . . . . . . . . 14 ⊢ u ∈ V
4		visset 1350	. . . . . . . . . . . . . 14 ⊢ v ∈ V
5	1, 2, 3, 4	inf3lem5 3468	. . . . . . . . . . . . 13 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → ((u ∈ ω ∧ v ∈ u) → (F ‘v) ⊂ (F ‘u)))
6		dfpss2 1557	. . . . . . . . . . . . . 14 ⊢ ((F ‘v) ⊂ (F ‘u) ↔ ((F ‘v) ⊆ (F ‘u) ∧ ¬ (F ‘v) = (F ‘u)))
7	6	pm3.27bd 263	. . . . . . . . . . . . 13 ⊢ ((F ‘v) ⊂ (F ‘u) → ¬ (F ‘v) = (F ‘u))
8	5, 7	syl6 23	. . . . . . . . . . . 12 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → ((u ∈ ω ∧ v ∈ u) → ¬ (F ‘v) = (F ‘u)))
9	8	exp3a 292	. . . . . . . . . . 11 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → (u ∈ ω → (v ∈ u → ¬ (F ‘v) = (F ‘u))))
10	9	imp 277	. . . . . . . . . 10 ⊢ (((¬ x = ∅ ∧ x ⊆ ∪x) ∧ u ∈ ω) → (v ∈ u → ¬ (F ‘v) = (F ‘u)))
11	10	adantrl 311	. . . . . . . . 9 ⊢ (((¬ x = ∅ ∧ x ⊆ ∪x) ∧ (v ∈ ω ∧ u ∈ ω)) → (v ∈ u → ¬ (F ‘v) = (F ‘u)))
12	1, 2, 4, 3	inf3lem5 3468	. . . . . . . . . . . . 13 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → ((v ∈ ω ∧ u ∈ v) → (F ‘u) ⊂ (F ‘v)))
13		dfpss2 1557	. . . . . . . . . . . . . . 15 ⊢ ((F ‘u) ⊂ (F ‘v) ↔ ((F ‘u) ⊆ (F ‘v) ∧ ¬ (F ‘u) = (F ‘v)))
14	13	pm3.27bd 263	. . . . . . . . . . . . . 14 ⊢ ((F ‘u) ⊂ (F ‘v) → ¬ (F ‘u) = (F ‘v))
15		cleqcom 1103	. . . . . . . . . . . . . . 15 ⊢ ((F ‘u) = (F ‘v) ↔ (F ‘v) = (F ‘u))
16	15	negbii 162	. . . . . . . . . . . . . 14 ⊢ (¬ (F ‘u) = (F ‘v) ↔ ¬ (F ‘v) = (F ‘u))
17	14, 16	sylib 173	. . . . . . . . . . . . 13 ⊢ ((F ‘u) ⊂ (F ‘v) → ¬ (F ‘v) = (F ‘u))
18	12, 17	syl6 23	. . . . . . . . . . . 12 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → ((v ∈ ω ∧ u ∈ v) → ¬ (F ‘v) = (F ‘u)))
19	18	exp3a 292	. . . . . . . . . . 11 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → (v ∈ ω → (u ∈ v → ¬ (F ‘v) = (F ‘u))))
20	19	imp 277	. . . . . . . . . 10 ⊢ (((¬ x = ∅ ∧ x ⊆ ∪x) ∧ v ∈ ω) → (u ∈ v → ¬ (F ‘v) = (F ‘u)))
21	20	adantrr 312	. . . . . . . . 9 ⊢ (((¬ x = ∅ ∧ x ⊆ ∪x) ∧ (v ∈ ω ∧ u ∈ ω)) → (u ∈ v → ¬ (F ‘v) = (F ‘u)))
22	11, 21	jaod 329	. . . . . . . 8 ⊢ (((¬ x = ∅ ∧ x ⊆ ∪x) ∧ (v ∈ ω ∧ u ∈ ω)) → ((v ∈ u ∨ u ∈ v) → ¬ (F ‘v) = (F ‘u)))
23	22	con2d 83	. . . . . . 7 ⊢ (((¬ x = ∅ ∧ x ⊆ ∪x) ∧ (v ∈ ω ∧ u ∈ ω)) → ((F ‘v) = (F ‘u) → ¬ (v ∈ u ∨ u ∈ v)))
24		ordtri3 2234	. . . . . . . . 9 ⊢ ((Ord v ∧ Ord u) → (v = u ↔ ¬ (v ∈ u ∨ u ∈ v)))
25		nnord 2381	. . . . . . . . 9 ⊢ (v ∈ ω → Ord v)
26		nnord 2381	. . . . . . . . 9 ⊢ (u ∈ ω → Ord u)
27	24, 25, 26	syl2an 349	. . . . . . . 8 ⊢ ((v ∈ ω ∧ u ∈ ω) → (v = u ↔ ¬ (v ∈ u ∨ u ∈ v)))
28	27	adantl 305	. . . . . . 7 ⊢ (((¬ x = ∅ ∧ x ⊆ ∪x) ∧ (v ∈ ω ∧ u ∈ ω)) → (v = u ↔ ¬ (v ∈ u ∨ u ∈ v)))
29	23, 28	sylibrd 179	. . . . . 6 ⊢ (((¬ x = ∅ ∧ x ⊆ ∪x) ∧ (v ∈ ω ∧ u ∈ ω)) → ((F ‘v) = (F ‘u) → v = u))
30	29	exp 291	. . . . 5 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → ((v ∈ ω ∧ u ∈ ω) → ((F ‘v) = (F ‘u) → v = u)))
31	30	19.21aivv 944	. . . 4 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → ∀v∀u((v ∈ ω ∧ u ∈ ω) → ((F ‘v) = (F ‘u) → v = u)))
32		r2al 1231	. . . 4 ⊢ (∀v ∈ ω ∀u ∈ ω ((F ‘v) = (F ‘u) → v = u) ↔ ∀v∀u((v ∈ ω ∧ u ∈ ω) → ((F ‘v) = (F ‘u) → v = u)))
33	31, 32	sylibr 175	. . 3 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → ∀v ∈ ω ∀u ∈ ω ((F ‘v) = (F ‘u) → v = u))
34		frfnom 2989	. . . . . . 7 ⊢ (rec(G, ∅) ↾ ω) Fn ω
35		fneq1 2718	. . . . . . 7 ⊢ (F = (rec(G, ∅) ↾ ω) → (F Fn ω ↔ (rec(G, ∅) ↾ ω) Fn ω))
36	34, 35	mpbiri 169	. . . . . 6 ⊢ (F = (rec(G, ∅) ↾ ω) → F Fn ω)
37	2, 36	ax-mp 6	. . . . 5 ⊢ F Fn ω
38		fvelrn 2883	. . . . . . . 8 ⊢ (F Fn ω → (u ∈ ran F ↔ ∃v ∈ ω (F ‘v) = u))
39		eleq1 1149	. . . . . . . . . . 11 ⊢ ((F ‘v) = u → ((F ‘v) ∈ ℘x ↔ u ∈ ℘x))
40		inf3lem.4	. . . . . . . . . . . . 13 ⊢ B ∈ V
41	1, 2, 4, 40	inf3lemd 3463	. . . . . . . . . . . 12 ⊢ (v ∈ ω → (F ‘v) ⊆ x)
42		fvex 2838	. . . . . . . . . . . . 13 ⊢ (F ‘v) ∈ V
43	42	elpw 1801	. . . . . . . . . . . 12 ⊢ ((F ‘v) ∈ ℘x ↔ (F ‘v) ⊆ x)
44	41, 43	sylibr 175	. . . . . . . . . . 11 ⊢ (v ∈ ω → (F ‘v) ∈ ℘x)
45	39, 44	syl5bi 183	. . . . . . . . . 10 ⊢ ((F ‘v) = u → (v ∈ ω → u ∈ ℘x))
46	45	com12 13	. . . . . . . . 9 ⊢ (v ∈ ω → ((F ‘v) = u → u ∈ ℘x))
47	46	r19.23aiv 1284	. . . . . . . 8 ⊢ (∃v ∈ ω (F ‘v) = u → u ∈ ℘x)
48	38, 47	syl6bi 187	. . . . . . 7 ⊢ (F Fn ω → (u ∈ ran F → u ∈ ℘x))
49	48	ssrdv 1509	. . . . . 6 ⊢ (F Fn ω → ran F ⊆ ℘x)
50	49	ancli 244	. . . . 5 ⊢ (F Fn ω → (F Fn ω ∧ ran F ⊆ ℘x))
51	37, 50	ax-mp 6	. . . 4 ⊢ (F Fn ω ∧ ran F ⊆ ℘x)
52		df-f 2434	. . . 4 ⊢ (F:ω–→℘x ↔ (F Fn ω ∧ ran F ⊆ ℘x))
53	51, 52	mpbir 165	. . 3 ⊢ F:ω–→℘x
54	33, 53	jctil 240	. 2 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → (F:ω–→℘x ∧ ∀v ∈ ω ∀u ∈ ω ((F ‘v) = (F ‘u) → v = u)))
55		f1fv 2916	. 2 ⊢ (F:ω–1-1→℘x ↔ (F:ω–→℘x ∧ ∀v ∈ ω ∀u ∈ ω ((F ‘v) = (F ‘u) → v = u)))
56	54, 55	sylibr 175	1 ⊢ ((¬ x = ∅ ∧ x ⊆ ∪x) → F:ω–1-1→℘x)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196  ∀wal 672   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  {crab 1204  Vcvv 1348   ∩ cin 1486   ⊆ wss 1487   ⊂ wpss 1488  ∅c0 1707  ℘cpw 1798  ∪cuni 1919  {copab 2055  Ord word 2198  ωcom 2372  ran crn 2411   ↾ cres 2412   Fn wfn 2417  –→wf 2418  –1-1→wf1 2419   ‘cfv 2422  reccrdg 2969

This theorem is referenced by:  inf3lem7 3470

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-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970

metamath.org