fin1a2lem12 - Metamath Proof Explorer

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

Theorem fin1a2lem12 10383

Description: Lemma for fin1a2 10387. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)

**Assertion**
Ref	Expression
fin1a2lem12	⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Proof of Theorem fin1a2lem12 Dummy variables 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 489	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐵 ∈ Fin^III)
2		simpll1 1229	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ⊆ 𝒫 𝐵)
3	2	adantr 485	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → 𝐴 ⊆ 𝒫 𝐵)
4		ssrab2 4036	. . . . . . . 8 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐴
5	4	unissi 4876	. . . . . . 7 ⊢ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ ∪ 𝐴
6		sspwuni 5061	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)
7	6	biimpi 219	. . . . . . 7 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ 𝐴 ⊆ 𝐵)
8	5, 7	sstrid 3950	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
9	3, 8	syl 18	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
10		elpw2g 5293	. . . . . 6 ⊢ (𝐵 ∈ Fin^III → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
11	10	ad2antlr 739	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
12	9, 11	mpbird 260	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵)
13	12	fmpttd 7100	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵)
14		vex 3461	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
15	14	sucex 7793	. . . . . . . . . 10 ⊢ suc 𝑑 ∈ V
16		sssucid 6432	. . . . . . . . . 10 ⊢ 𝑑 ⊆ suc 𝑑
17		ssdomg 8985	. . . . . . . . . 10 ⊢ (suc 𝑑 ∈ V → (𝑑 ⊆ suc 𝑑 → 𝑑 ≼ suc 𝑑))
18	15, 16, 17	mp2 9	. . . . . . . . 9 ⊢ 𝑑 ≼ suc 𝑑
19		domtr 8992	. . . . . . . . 9 ⊢ ((𝑓 ≼ 𝑑 ∧ 𝑑 ≼ suc 𝑑) → 𝑓 ≼ suc 𝑑)
20	18, 19	mpan2 703	. . . . . . . 8 ⊢ (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑)
21	20	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐴 → (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑))
22	21	ss2rabi 4032	. . . . . 6 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑}
23		uniss 4875	. . . . . 6 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
24	22, 23	mp1i 14	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
25		id 23	. . . . . 6 ⊢ (𝑑 ∈ ω → 𝑑 ∈ ω)
26		pwexg 5339	. . . . . . . . 9 ⊢ (𝐵 ∈ Fin^III → 𝒫 𝐵 ∈ V)
27	26	adantl 486	. . . . . . . 8 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝒫 𝐵 ∈ V)
28	27, 2	ssexd 5284	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ∈ V)
29		rabexg 5297	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
30		uniexg 7727	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
31	28, 29, 30	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
32		breq2 5108	. . . . . . . . 9 ⊢ (𝑒 = 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ 𝑑))
33	32	rabbidv 3424	. . . . . . . 8 ⊢ (𝑒 = 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
34	33	unieqd 4880	. . . . . . 7 ⊢ (𝑒 = 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
35		eqid 2765	. . . . . . 7 ⊢ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})
36	34, 35	fvmptg 6977	. . . . . 6 ⊢ ((𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
37	25, 31, 36	syl2anr 608	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
38		peano2 7874	. . . . . 6 ⊢ (𝑑 ∈ ω → suc 𝑑 ∈ ω)
39		rabexg 5297	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
40		uniexg 7727	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
41	28, 39, 40	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
42		breq2 5108	. . . . . . . . 9 ⊢ (𝑒 = suc 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ suc 𝑑))
43	42	rabbidv 3424	. . . . . . . 8 ⊢ (𝑒 = suc 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
44	43	unieqd 4880	. . . . . . 7 ⊢ (𝑒 = suc 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
45	44, 35	fvmptg 6977	. . . . . 6 ⊢ ((suc 𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
46	38, 41, 45	syl2anr 608	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
47	24, 37, 46	3sstr4d 3994	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
48	47	ralrimiva 3157	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
49		fin34i 10353	. . 3 ⊢ ((𝐵 ∈ Fin^III ∧ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵 ∧ ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑)) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
50	1, 13, 48, 49	syl3anc 1394	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
51		fin1a2lem11 10382	. . . . . 6 ⊢ (( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
52	51	adantrr 729	. . . . 5 ⊢ (( [⊊] Or 𝐴 ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
53	52	3ad2antl2 1203	. . . 4 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
54	53	adantr 485	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
55		simpll3 1231	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 ∈ 𝐴)
56		simplrr 789	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ≠ ∅)
57		sspwuni 5061	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 ⊆ ∅)
58		ss0b 4358	. . . . . . . . . . 11 ⊢ (∪ 𝐴 ⊆ ∅ ↔ ∪ 𝐴 = ∅)
59	57, 58	bitri 278	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 = ∅)
60		pw0 4773	. . . . . . . . . . . . 13 ⊢ 𝒫 ∅ = {∅}
61	60	sseq2i 3968	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 ⊆ {∅})
62		sssn 4787	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ {∅} ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
63	61, 62	bitri 278	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
64		df-ne 2961	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
65		0ex 5261	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
66	65	unisn 4886	. . . . . . . . . . . . . . . 16 ⊢ ∪ {∅} = ∅
67	65	snid 4624	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ {∅}
68	66, 67	eqeltri 2861	. . . . . . . . . . . . . . 15 ⊢ ∪ {∅} ∈ {∅}
69		unieq 4878	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → ∪ 𝐴 = ∪ {∅})
70		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → 𝐴 = {∅})
71	69, 70	eleq12d 2859	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = {∅} → (∪ 𝐴 ∈ 𝐴 ↔ ∪ {∅} ∈ {∅}))
72	68, 71	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ (𝐴 = {∅} → ∪ 𝐴 ∈ 𝐴)
73	72	orim2i 923	. . . . . . . . . . . . 13 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 = ∅ ∨ ∪ 𝐴 ∈ 𝐴))
74	73	ord 877	. . . . . . . . . . . 12 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (¬ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
75	64, 74	biimtrid 245	. . . . . . . . . . 11 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
76	63, 75	sylbi 220	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
77	59, 76	sylbir 238	. . . . . . . . 9 ⊢ (∪ 𝐴 = ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
78	77	com12 33	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → (∪ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
79	78	con3d 153	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → (¬ ∪ 𝐴 ∈ 𝐴 → ¬ ∪ 𝐴 = ∅))
80	56, 55, 79	sylc 66	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 = ∅)
81		ioran 999	. . . . . 6 ⊢ (¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅) ↔ (¬ ∪ 𝐴 ∈ 𝐴 ∧ ¬ ∪ 𝐴 = ∅))
82	55, 80, 81	sylanbrc 594	. . . . 5 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
83		uniun 4890	. . . . . . . 8 ⊢ ∪ (𝐴 ∪ {∅}) = (∪ 𝐴 ∪ ∪ {∅})
84	66	uneq2i 4121	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∪ {∅}) = (∪ 𝐴 ∪ ∅)
85		un0 4351	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∅) = ∪ 𝐴
86	83, 84, 85	3eqtri 2792	. . . . . . 7 ⊢ ∪ (𝐴 ∪ {∅}) = ∪ 𝐴
87	86	eleq1i 2856	. . . . . 6 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ ∪ 𝐴 ∈ (𝐴 ∪ {∅}))
88		elun 4109	. . . . . 6 ⊢ (∪ 𝐴 ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}))
89	65	elsn2 4627	. . . . . . 7 ⊢ (∪ 𝐴 ∈ {∅} ↔ ∪ 𝐴 = ∅)
90	89	orbi2i 925	. . . . . 6 ⊢ ((∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
91	87, 88, 90	3bitri 300	. . . . 5 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
92	82, 91	sylnibr 332	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}))
93		unieq 4878	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = ∪ (𝐴 ∪ {∅}))
94		id 23	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
95	93, 94	eleq12d 2859	. . . . 5 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
96	95	notbid 321	. . . 4 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
97	92, 96	syl5ibrcom 250	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})))
98	54, 97	mpd 16	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
99	50, 98	pm2.65da 828	1 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∀wral 3079 {crab 3417 Vcvv 3457 ∪ cun 3905 ⊆ wss 3907 ∅c0 4288 𝒫 cpw 4558 {csn 4585 ∪ cuni 4867 class class class wbr 5104 ↦ cmpt 5185 Or wor 5558 ran crn 5652 suc csuc 6351 ⟶wf 6521 ‘cfv 6525 [⊊] crpss 7709 ωcom 7850 ≼ cdom 8929 Fincfn 8931 Fin^IIIcfin3 10253

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4908 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-rpss 7710 df-om 7851 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-wdom 9515 df-card 9913 df-fin4 10259 df-fin3 10260

This theorem is referenced by: fin1a2s 10386

W3C validator